src/Pure/goal.ML
changeset 32738 15bb09ca0378
parent 32365 9b74d0339c44
child 32788 a65deb8f9434
--- a/src/Pure/goal.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/goal.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -6,7 +6,7 @@
 
 signature BASIC_GOAL =
 sig
-  val parallel_proofs: int ref
+  val parallel_proofs: int Unsynchronized.ref
   val SELECT_GOAL: tactic -> int -> tactic
   val CONJUNCTS: tactic -> int -> tactic
   val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
@@ -102,7 +102,7 @@
 
 (* future_enabled *)
 
-val parallel_proofs = ref 1;
+val parallel_proofs = Unsynchronized.ref 1;
 
 fun future_enabled () =
   Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;