src/HOL/Tools/refute.ML

       val u      = unfold_defs thy t
       val _      = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u)
       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)))
       (* we can only consider fragments of recursive IDTs, so we issue a  *)
       (* warning if the formula contains a recursive IDT                  *)