# HG changeset patch
# User wenzelm
# Date 1231161760 -3600
# Node ID c7735554d291c185f7f10c406ef07705dfe744cc
# Parent  b49d8501720a9ec3ce9469af067fa65a2f6416ad
added future_terminal_proof;

diff -r b49d8501720a -r c7735554d291 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Jan 05 00:13:11 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Jan 05 14:22:40 2009 +0100
@@ -115,6 +115,7 @@
     ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
   val is_relevant: state -> bool
   val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
+  val future_terminal_proof: Method.text * Method.text option -> state -> context
 end;
 
 structure Proof: PROOF =
@@ -1027,5 +1028,10 @@
 
 end;
 
+fun future_terminal_proof meths state =
+  if is_relevant state then global_terminal_proof meths state
+  else #2 (state |> future_proof (fn state' =>
+    Future.fork_pri ~1 (fn () => ((), global_terminal_proof meths state'))));
+
 end;