src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
changeset 32740 9dd0a2f83429
parent 32646 962b4354ed90
child 32828 ad76967c703d
     1.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    val sos_tac : (RealArith.pss_tree -> unit) ->
     1.5      proof_method -> Proof.context -> int -> tactic
     1.6  
     1.7 -  val debugging : bool ref;
     1.8 +  val debugging : bool Unsynchronized.ref;
     1.9    
    1.10    exception Failure of string;
    1.11  end
    1.12 @@ -58,7 +58,7 @@
    1.13  val pow2 = rat_pow rat_2;
    1.14  val pow10 = rat_pow rat_10;
    1.15  
    1.16 -val debugging = ref false;
    1.17 +val debugging = Unsynchronized.ref false;
    1.18  
    1.19  exception Sanity;
    1.20