--- a/src/HOL/Tools/res_axioms.ML Tue Oct 20 16:13:01 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML Wed Oct 21 08:14:38 2009 +0200
@@ -476,7 +476,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 (gen_union (op aconv)) [] (map OldTerm.term_frees remaining_hyps)
+ List.foldl (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;