# HG changeset patch
# User berghofe
# Date 1207237381 -7200
# Node ID 777f334ff652aefc0f3ce244fe978c8b7a106b4c
# Parent  03ad378ed5f0affb5d667a29145ae2b41dd9efe9
Added prove_global.

diff -r 03ad378ed5f0 -r 777f334ff652 src/Pure/Isar/skip_proof.ML
--- 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;