--- a/src/Pure/pattern.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/pattern.ML Tue Sep 29 11:49:22 2009 +0200
@@ -14,7 +14,7 @@
signature PATTERN =
sig
- val trace_unify_fail: bool ref
+ val trace_unify_fail: bool Unsynchronized.ref
val aeconv: term * term -> bool
val eta_long: typ list -> term -> term
val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
@@ -40,7 +40,7 @@
exception Unif;
exception Pattern;
-val trace_unify_fail = ref false;
+val trace_unify_fail = Unsynchronized.ref false;
fun string_of_term thy env binders t =
Syntax.string_of_term_global thy