Added prove_global.

--- a/src/Pure/Isar/skip_proof.ML	Thu Apr 03 16:34:52 2008 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Thu Apr 03 17:43:01 2008 +0200
@@ -11,6 +11,8 @@
   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 =
@@ -42,4 +44,7 @@
     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;