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