--- a/src/HOL/Tools/res_axioms.ML Wed Oct 21 12:02:19 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML Wed Oct 21 12:02:56 2009 +0200
@@ -473,7 +473,7 @@
val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
(map Thm.term_of hyps)
val fixed = OldTerm.term_frees (concl_of st) @
- List.foldl (union (op aconv)) [] (map OldTerm.term_frees remaining_hyps)
+ List.foldl (uncurry (union (op aconv))) [] (map OldTerm.term_frees remaining_hyps)
in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;