src/Pure/goal.ML

 
 fun prove_future ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac);
 fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
 
 fun prove_global thy xs asms prop tac =
-  Drule.standard (prove (ProofContext.init thy) xs asms prop tac);
+  Drule.export_without_context (prove (ProofContext.init thy) xs asms prop tac);
 
 
 
 (** goal structure **)