src/Pure/Isar/skip_proof.ML

 sig
   val make_thm: theory -> term -> thm
   val cheat_tac: theory -> tactic
   val prove: Proof.context -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
+  val prove_global: theory -> string list -> term list -> term ->
+    (thm list -> tactic) -> thm
 end;
 
 structure SkipProof: SKIP_PROOF =
 struct
 

   Goal.prove ctxt xs asms prop (fn args => fn st =>
     if ! quick_and_dirty
     then setmp quick_and_dirty true (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 (fn {prems, ...} => tac prems));
+
 end;