--- a/src/HOL/Tools/res_clause.ML Wed Oct 21 12:02:19 2009 +0200
+++ b/src/HOL/Tools/res_clause.ML Wed Oct 21 12:02:56 2009 +0200
@@ -93,7 +93,7 @@
val tconst_prefix = "tc_";
val class_prefix = "class_";
-fun union_all xss = List.foldl (union (op =)) [] xss;
+fun union_all xss = List.foldl (uncurry (union (op =))) [] xss;
(*Provide readable names for the more common symbolic functions*)
val const_trans_table =
@@ -263,7 +263,7 @@
| 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 (union (op =)) [] (map sorts_on_typs Ts);
+fun add_typs Ts = List.foldl (uncurry (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
@@ -372,7 +372,7 @@
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 (union (op =) (classes', classes), union (op =) (cpairs', cpairs)) end;
+ in (union (op =) classes' classes, 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