src/Pure/goal.ML
changeset 35021 c839a4c670c6
parent 33768 bba9eac8aa25
child 35845 e5980f0ad025
     1.1 --- a/src/Pure/goal.ML	Sun Feb 07 19:31:55 2010 +0100
     1.2 +++ b/src/Pure/goal.ML	Sun Feb 07 19:33:34 2010 +0100
     1.3 @@ -210,7 +210,7 @@
     1.4  fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
     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  
    1.11