src/Pure/Isar/skip_proof.ML

       if ! quick_and_dirty
       then cheat_tac (ProofContext.theory_of ctxt) st
       else tac args st);
 
 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);
 
 end;