src/HOL/Tools/res_clause.ML

 
 val const_prefix = "c_";
 val tconst_prefix = "tc_";
 val class_prefix = "class_";
 
-fun union_all xss = List.foldl (op union) [] xss;
+fun union_all xss = List.foldl (gen_union (op =)) [] xss;
 
 (*Provide readable names for the more common symbolic functions*)
 val const_trans_table =
       Symtab.make [(@{const_name "op ="}, "equal"),
                    (@{const_name HOL.less_eq}, "lessequals"),

 
 fun pred_of_sort (LTVar (s,ty)) = (s,1)
   | pred_of_sort (LTFree (s,ty)) = (s,1)
 
 (*Given a list of sorted type variables, return a list of type literals.*)
-fun add_typs Ts = List.foldl (op union) [] (map sorts_on_typs Ts);
+fun add_typs Ts = List.foldl (gen_union (op =)) [] (map sorts_on_typs Ts);
 
 (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
   * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
     in a lemma has the same sort as 'a in the conjecture.
   * Deleting such clauses will lead to problems with locales in other use of local results

 fun iter_type_class_pairs thy tycons [] = ([], [])
   | iter_type_class_pairs thy tycons classes =
       let val cpairs = type_class_pairs thy tycons classes
           val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) \\ classes \\ HOLogic.typeS
           val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
-      in  (classes' union classes, cpairs' union cpairs)  end;
+      in (gen_union (op =) (classes', classes), gen_union (op =) (cpairs', cpairs)) end;
 
 fun make_arity_clauses_dfg dfg thy tycons classes =
   let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
   in  (classes', multi_arity_clause dfg cpairs)  end;
 val make_arity_clauses = make_arity_clauses_dfg false;