diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Tue Sep 29 14:59:24 2009 +0200
+++ b/src/FOLP/simp.ML	Tue Sep 29 16:24:36 2009 +0200
@@ -49,7 +49,7 @@
 (* temporarily disabled:
   val extract_free_congs        : unit -> thm list
 *)
-  val tracing   : bool ref
+  val tracing   : bool Unsynchronized.ref
 end;
 
 functor SimpFun (Simp_data: SIMP_DATA) : SIMP =
@@ -366,7 +366,7 @@
 
 (** Tracing **)
 
-val tracing = ref false;
+val tracing = Unsynchronized.ref false;
 
 (*Replace parameters by Free variables in P*)
 fun variants_abs ([],P) = P