# HG changeset patch
# User wenzelm
# Date 1360852473 -3600
# Node ID 32a5994dd205148853903b775c46a64c570c38ca
# Parent  2e1bc14724b5bd21f7a0cc06cca1db825212c2e0
tuned signature -- legacy packages might want to fork proofs as well;

diff -r 2e1bc14724b5 -r 32a5994dd205 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Feb 14 13:16:47 2013 +0100
+++ b/src/Pure/goal.ML	Thu Feb 14 15:34:33 2013 +0100
@@ -39,6 +39,8 @@
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val prove: Proof.context -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
+  val prove_global_future: theory -> string list -> term list -> term ->
+    ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val prove_global: theory -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val extract: int -> int -> thm -> thm Seq.seq
@@ -294,8 +296,12 @@
 val prove_multi = prove_common true;
 
 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_future thy xs asms prop tac =
+  Drule.export_without_context (prove_future (Proof_Context.init_global thy) xs asms prop tac);
+
 fun prove_global thy xs asms prop tac =
   Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);