src/HOL/Import/proof_kernel.ML

 fun i mem L =
     let fun itr [] = false
           | itr (a::rst) = i=a orelse itr rst
     in itr L end;
 
+infix union;
 fun [] union S = S
   | S union [] = S
-  | (a::rst) union S2 = rst union (insert (op =) a S2)
+  | (a::rst) union S2 = rst union (insert (op =) a S2);
 
 fun implode_subst [] = []
   | implode_subst (x::r::rest) = ((x,r)::(implode_subst rest))
   | implode_subst _ = raise ERR "implode_subst" "malformed substitution list"
 

           | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
           | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
           | add_consts (_, cs) = cs
         val t_consts = add_consts(t,[])
     in
-        fn th => eq_set(t_consts,add_consts(prop_of th,[]))
+        fn th => gen_eq_set (op =) (t_consts, add_consts (prop_of th, []))
     end
 
 fun split_name str =
     let
         val sub = Substring.full str