src/Pure/goal.ML
changeset 32738 15bb09ca0378
parent 32365 9b74d0339c44
child 32788 a65deb8f9434
     1.1 --- a/src/Pure/goal.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/goal.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature BASIC_GOAL =
     1.6  sig
     1.7 -  val parallel_proofs: int ref
     1.8 +  val parallel_proofs: int Unsynchronized.ref
     1.9    val SELECT_GOAL: tactic -> int -> tactic
    1.10    val CONJUNCTS: tactic -> int -> tactic
    1.11    val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
    1.12 @@ -102,7 +102,7 @@
    1.13  
    1.14  (* future_enabled *)
    1.15  
    1.16 -val parallel_proofs = ref 1;
    1.17 +val parallel_proofs = Unsynchronized.ref 1;
    1.18  
    1.19  fun future_enabled () =
    1.20    Multithreading.enabled () andalso Future.is_worker () andalso ! parallel_proofs >= 1;