removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);
--- a/src/Pure/Isar/proof.ML Fri Aug 06 12:38:02 2010 +0200
+++ b/src/Pure/Isar/proof.ML Fri Aug 06 14:35:04 2010 +0200
@@ -1074,8 +1074,7 @@
local
fun future_terminal_proof proof1 proof2 meths int state =
- if not (Goal.local_future_enforced ()) andalso
- int orelse is_relevant state orelse not (Goal.local_future_enabled ())
+ if int orelse is_relevant state orelse not (Goal.local_future_enabled ())
then proof1 meths state
else snd (proof2 (fn state' => Goal.fork (fn () => ((), proof1 meths state'))) state);
--- a/src/Pure/goal.ML Fri Aug 06 12:38:02 2010 +0200
+++ b/src/Pure/goal.ML Fri Aug 06 14:35:04 2010 +0200
@@ -26,7 +26,6 @@
val fork: (unit -> 'a) -> 'a future
val future_enabled: unit -> bool
val local_future_enabled: unit -> bool
- val local_future_enforced: unit -> bool
val future_result: Proof.context -> thm future -> term -> thm
val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
val prove_multi: Proof.context -> string list -> term list -> term list ->
@@ -112,7 +111,6 @@
Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;
fun local_future_enabled () = future_enabled () andalso ! parallel_proofs >= 2;
-fun local_future_enforced () = future_enabled () andalso ! parallel_proofs >= 3;
(* future_result *)