src/ZF/Datatype.ML

--- a/src/ZF/Datatype.ML	Sat Jul 08 12:54:36 2006 +0200
+++ b/src/ZF/Datatype.ML	Sat Jul 08 12:54:37 2006 +0200
@@ -87,7 +87,8 @@
                  writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
                else ();
        val goal = Logic.mk_equals (old, new)
-       val thm = Goal.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
+       val thm = Goal.prove (Simplifier.the_context ss) [] [] goal
+         (fn _ => rtac iff_reflection 1 THEN
            simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
          handle ERROR msg =>
          (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);