src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
changeset 32740 9dd0a2f83429
parent 32646 962b4354ed90
child 32944 ecc0705174c2
     1.1 --- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4    datatype prover_result = Success | Failure | Error
     1.5  
     1.6    val setup: theory -> theory
     1.7 -  val destdir: string ref
     1.8 +  val destdir: string Unsynchronized.ref
     1.9    val get_prover_name: unit -> string
    1.10    val set_prover_name: string -> unit
    1.11  end
    1.12 @@ -30,7 +30,7 @@
    1.13  
    1.14  (*** calling provers ***)
    1.15  
    1.16 -val destdir = ref ""
    1.17 +val destdir = Unsynchronized.ref ""
    1.18  
    1.19  fun filename dir name =
    1.20    let
    1.21 @@ -113,7 +113,7 @@
    1.22  
    1.23  (* default prover *)
    1.24  
    1.25 -val prover_name = ref "remote_csdp"
    1.26 +val prover_name = Unsynchronized.ref "remote_csdp"
    1.27  
    1.28  fun get_prover_name () = CRITICAL (fn () => ! prover_name);
    1.29  fun set_prover_name str = CRITICAL (fn () => prover_name := str);