src/HOL/Tools/ATP/recon_transfer_proof.ML

 |   assoc_out_of_order a ((b,c)::t) = if there_out_of_order a c then b else assoc_out_of_order a t;
 
 fun get_assoc_snds [] xs assocs= assocs
 |   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_out_of_order x ys))])
 
-fun add_if_not_inlist [] xs newlist = newlist
-|   add_if_not_inlist (y::ys) xs newlist = if (not (y mem xs)) then 
-                                      add_if_not_inlist ys xs (y::newlist)
-                                        else add_if_not_inlist ys xs (newlist)
+fun add_if_not_inlist eq [] xs newlist = newlist
+|   add_if_not_inlist eq (y::ys) xs newlist =
+    if not (member eq xs y) then add_if_not_inlist eq ys xs (y::newlist)
+    else add_if_not_inlist eq ys xs newlist
 
 (*Flattens a list of list of strings to one string*)
 fun onestr ls = String.concat (map String.concat ls);
 
 fun is_clasimp_ax clasimp_num n = n <= clasimp_num 

      val ax_metas = get_assoc_snds ax_strs metas_and_strs []
      val ax_vars = map thm_vars ax_metas
      val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
 
      (* get list of extra axioms as thms with their variables *)
-     val extra_metas = add_if_not_inlist metas ax_metas []
+     val extra_metas = add_if_not_inlist Thm.eq_thm metas ax_metas []
      val extra_vars = map thm_vars extra_metas
-     val extra_with_vars = if (not (extra_metas = []) ) 
+     val extra_with_vars = if not (null extra_metas)
 			   then ListPair.zip (extra_metas,extra_vars)
 			   else []
  in
     (distfrees,distvars, extra_with_vars,ax_with_vars, ListPair.zip (step_nums,ax_metas))
  end;

       val ax_strs = map ReconOrderClauses.get_meta_lits_bracket (map #2 numcls)
       val numcls_strs = ListPair.zip (ax_nums,ax_strs)
       val num_cls_vars =  map (addvars vars) numcls_strs;
       val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
       
-      val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars))
+      val extra_nums = if not (null extra_with_vars) then (1 upto (length extra_with_vars))
                        else []
       val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
       val frees_str = "["^(thmvars_to_string frees "")^"]"
       val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
       val _ = trace ("\nReconstruction:\n" ^ reconstr)