src/HOL/Tools/prop_logic.ML
changeset 32740 9dd0a2f83429
parent 31220 f1c0ed85a33b
child 33029 2fefe039edf1
child 33037 b22e44496dc2
     1.1 --- a/src/HOL/Tools/prop_logic.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/Tools/prop_logic.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -292,7 +292,7 @@
     1.4  			val fm' = nnf fm
     1.5  			(* 'new' specifies the next index that is available to introduce an auxiliary variable *)
     1.6  			(* int ref *)
     1.7 -			val new = ref (maxidx fm' + 1)
     1.8 +			val new = Unsynchronized.ref (maxidx fm' + 1)
     1.9  			(* unit -> int *)
    1.10  			fun new_idx () = let val idx = !new in new := idx+1; idx end
    1.11  			(* replaces 'And' by an auxiliary variable (and its definition) *)
    1.12 @@ -381,15 +381,15 @@
    1.13  	(* Term.term -> int Termtab.table -> prop_formula * int Termtab.table *)
    1.14  	fun prop_formula_of_term t table =
    1.15  	let
    1.16 -		val next_idx_is_valid = ref false
    1.17 -		val next_idx          = ref 0
    1.18 +		val next_idx_is_valid = Unsynchronized.ref false
    1.19 +		val next_idx          = Unsynchronized.ref 0
    1.20  		fun get_next_idx () =
    1.21  			if !next_idx_is_valid then
    1.22 -				inc next_idx
    1.23 +				Unsynchronized.inc next_idx
    1.24  			else (
    1.25  				next_idx          := Termtab.fold (curry Int.max o snd) table 0;
    1.26  				next_idx_is_valid := true;
    1.27 -				inc next_idx
    1.28 +				Unsynchronized.inc next_idx
    1.29  			)
    1.30  		fun aux (Const ("True", _))         table =
    1.31  			(True, table)