# HG changeset patch
# User wenzelm
# Date 1281098104 -7200
# Node ID 1408f753bd751cf27f7f0bfc7f6f04f9cdc7aa3e
# Parent  c75e9dc841c72471333038ca17a9b89a4d6ce04c
removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);

diff -r c75e9dc841c7 -r 1408f753bd75 src/Pure/Isar/proof.ML
--- 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);
 
diff -r c75e9dc841c7 -r 1408f753bd75 src/Pure/goal.ML
--- 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 *)