src/ZF/ind_syntax.ML
changeset 35021 c839a4c670c6
parent 33317 b4534348b8fd
child 35129 ed24ba6f69aa
     1.1 --- a/src/ZF/ind_syntax.ML	Sun Feb 07 19:31:55 2010 +0100
     1.2 +++ b/src/ZF/ind_syntax.ML	Sun Feb 07 19:33:34 2010 +0100
     1.3 @@ -114,7 +114,7 @@
     1.4    | tryres (th, []) = raise THM("tryres", 0, [th]);
     1.5  
     1.6  fun gen_make_elim elim_rls rl =
     1.7 -      Drule.standard (tryres (rl, elim_rls @ [revcut_rl]));
     1.8 +  Drule.export_without_context (tryres (rl, elim_rls @ [revcut_rl]));
     1.9  
    1.10  (*Turns iff rules into safe elimination rules*)
    1.11  fun mk_free_SEs iffs = map (gen_make_elim [@{thm conjE}, @{thm FalseE}]) (iffs RL [@{thm iffD1}]);