diff -r fb577a13abbd -r 250cd2a9308d src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue May 21 17:45:53 2013 +0200
+++ b/src/Pure/goal.ML	Tue May 21 17:55:28 2013 +0200
@@ -8,8 +8,6 @@
 sig
   val skip_proofs: bool Unsynchronized.ref
   val parallel_proofs: int Unsynchronized.ref
-  val parallel_subproofs_saturation: int Unsynchronized.ref
-  val parallel_subproofs_threshold: real Unsynchronized.ref
   val SELECT_GOAL: tactic -> int -> tactic
   val CONJUNCTS: tactic -> int -> tactic
   val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
@@ -200,8 +198,6 @@
 val skip_proofs = Unsynchronized.ref false;
 
 val parallel_proofs = Unsynchronized.ref 1;
-val parallel_subproofs_saturation = Unsynchronized.ref 100;
-val parallel_subproofs_threshold = Unsynchronized.ref 0.01;
 
 fun future_enabled_level n =
   Multithreading.enabled () andalso ! parallel_proofs >= n andalso
@@ -211,10 +207,12 @@
 
 fun future_enabled_nested n =
   future_enabled_level n andalso
-  forked_count () < ! parallel_subproofs_saturation * Multithreading.max_threads_value ();
+  forked_count () <
+    Options.default_int "parallel_subproofs_saturation" * Multithreading.max_threads_value ();
 
 fun future_enabled_timing t =
-  future_enabled () andalso Time.toReal t >= ! parallel_subproofs_threshold;
+  future_enabled () andalso
+    Time.toReal t >= Options.default_real "parallel_subproofs_threshold";
 
 
 (* future_result *)