src/ZF/ind_syntax.ML

--- a/src/ZF/ind_syntax.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/ZF/ind_syntax.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -114,7 +114,7 @@
   | tryres (th, []) = raise THM("tryres", 0, [th]);
 
 fun gen_make_elim elim_rls rl =
-      Drule.standard (tryres (rl, elim_rls @ [revcut_rl]));
+  Drule.export_without_context (tryres (rl, elim_rls @ [revcut_rl]));
 
 (*Turns iff rules into safe elimination rules*)
 fun mk_free_SEs iffs = map (gen_make_elim [@{thm conjE}, @{thm FalseE}]) (iffs RL [@{thm iffD1}]);