src/ZF/Datatype_ZF.thy
changeset 32740 9dd0a2f83429
parent 32432 64f30bdd3ba1
child 32765 3032c0308019
     1.1 --- a/src/ZF/Datatype_ZF.thy	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/ZF/Datatype_ZF.thy	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -59,7 +59,7 @@
     1.4  (*Simproc for freeness reasoning: compare datatype constructors for equality*)
     1.5  structure DataFree =
     1.6  struct
     1.7 -  val trace = ref false;
     1.8 +  val trace = Unsynchronized.ref false;
     1.9  
    1.10    fun mk_new ([],[]) = Const("True",FOLogic.oT)
    1.11      | mk_new (largs,rargs) =