diff --git a/ProofTrace/fusion.ml.diff b/ProofTrace/fusion.ml.diff
index 75f9034..c93e114 100644
--- a/ProofTrace/fusion.ml.diff
+++ b/ProofTrace/fusion.ml.diff
@@ -1,5 +1,5 @@
 diff --git a/fusion.ml b/fusion.ml
-index a08ad1c..7d67f20 100644
+index 93a0d51..f072934 100644
 --- a/fusion.ml
 +++ b/fusion.ml
 @@ -23,6 +23,23 @@ module type Hol_kernel =
@@ -239,7 +239,7 @@ index a08ad1c..7d67f20 100644
      else failwith "new_axiom: Not a proposition"

  (* ------------------------------------------------------------------------- *)
-@@ -593,8 +687,11 @@ module Hol : Hol_kernel = struct
+@@ -595,8 +689,11 @@ module Hol : Hol_kernel = struct
          else if not (subset (type_vars_in_term r) (tyvars ty))
          then failwith "new_definition: Type variables not reflected in constant"
          else let c = new_constant(cname,ty); Const(cname,ty) in
@@ -250,10 +250,10 @@ index a08ad1c..7d67f20 100644
 +             let dth = Sequent([],dtm,idx) in
 +             (the_definitions := dth::(!the_definitions);
 +              new_proof (Proof(idx,dth,Pdef(dtm,cname,ty))))
+     | Comb(Comb(Const("=",_),Const(cname,ty)),r) ->
+       failwith ("new_basic_definition: '" ^ cname ^ "' is already defined")
      | _ -> failwith "new_basic_definition"
-
- (* ------------------------------------------------------------------------- *)
-@@ -610,7 +707,7 @@ module Hol : Hol_kernel = struct
+@@ -614,7 +711,7 @@ module Hol : Hol_kernel = struct
  (* Where "abs" and "rep" are new constants with the nominated names.         *)
  (* ------------------------------------------------------------------------- *)

@@ -262,7 +262,7 @@ index a08ad1c..7d67f20 100644
      if exists (can get_const_type) [absname; repname] then
        failwith "new_basic_type_definition: Constant(s) already in use" else
      if not (asl = []) then
-@@ -630,9 +727,19 @@ module Hol : Hol_kernel = struct
+@@ -634,9 +731,19 @@ module Hol : Hol_kernel = struct
      let abs = (new_constant(absname,absty); Const(absname,absty))
      and rep = (new_constant(repname,repty); Const(repname,repty)) in
      let a = Var("a",aty) and r = Var("r",rty) in