src/HOL/Tools/refute.ML
changeset 33042 ddf1f03a9ad9
parent 33039 5018f6a76b3f
child 33055 5a733f325939
--- a/src/HOL/Tools/refute.ML	Wed Oct 21 12:02:19 2009 +0200
+++ b/src/HOL/Tools/refute.ML	Wed Oct 21 12:02:56 2009 +0200
@@ -1154,7 +1154,7 @@
       val axioms = collect_axioms thy u
       (* Term.typ list *)
       val types = Library.foldl (fn (acc, t') =>
-        union (op =) (acc, (ground_types thy t'))) ([], u :: axioms)
+        uncurry (union (op =)) (acc, (ground_types thy t'))) ([], u :: axioms)
       val _     = tracing ("Ground types: "
         ^ (if null types then "none."
            else commas (map (Syntax.string_of_typ_global thy) types)))