--- 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;