src/Tools/eqsubst.ML
changeset 32740 9dd0a2f83429
parent 32149 ef59550a55d3
child 32960 69916a850301
--- a/src/Tools/eqsubst.ML	Tue Sep 29 14:59:24 2009 +0200
+++ b/src/Tools/eqsubst.ML	Tue Sep 29 16:24:36 2009 +0200
@@ -278,8 +278,8 @@
              * (string * typ) list (* Type abs env *)
              * term) (* outer term *);
 
-val trace_subst_err = (ref NONE : trace_subst_errT option ref);
-val trace_subst_search = ref false;
+val trace_subst_err = (Unsynchronized.ref NONE : trace_subst_errT option Unsynchronized.ref);
+val trace_subst_search = Unsynchronized.ref false;
 exception trace_subst_exp of trace_subst_errT;
 *)