src/HOL/Tools/cnf_funcs.ML
changeset 32740 9dd0a2f83429
parent 32283 3bebc195c124
child 32960 69916a850301
     1.1 --- a/src/HOL/Tools/cnf_funcs.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -399,12 +399,10 @@
     1.4  
     1.5  fun make_cnfx_thm thy t =
     1.6  let
     1.7 -	val var_id = ref 0  (* properly initialized below *)
     1.8 -	(* unit -> Term.term *)
     1.9 +	val var_id = Unsynchronized.ref 0  (* properly initialized below *)
    1.10  	fun new_free () =
    1.11 -		Free ("cnfx_" ^ string_of_int (inc var_id), HOLogic.boolT)
    1.12 -	(* Term.term -> Thm.thm *)
    1.13 -	fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) =
    1.14 +		Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
    1.15 +	fun make_cnfx_thm_from_nnf (Const ("op &", _) $ x $ y) : thm =
    1.16  		let
    1.17  			val thm1 = make_cnfx_thm_from_nnf x
    1.18  			val thm2 = make_cnfx_thm_from_nnf y