src/Pure/Isar/skip_proof.ML
changeset 35021 c839a4c670c6
parent 32970 fbd2bb2489a8
child 36610 bafd82950e24
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Sun Feb 07 19:31:55 2010 +0100
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Sun Feb 07 19:33:34 2010 +0100
     1.3 @@ -39,6 +39,6 @@
     1.4        else tac args st);
     1.5  
     1.6  fun prove_global thy xs asms prop tac =
     1.7 -  Drule.standard (prove (ProofContext.init thy) xs asms prop tac);
     1.8 +  Drule.export_without_context (prove (ProofContext.init thy) xs asms prop tac);
     1.9  
    1.10  end;