diff -r 1476fe841023 -r ea6672bff5dd src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Tue Sep 29 14:26:33 2009 +1000
+++ b/src/HOL/Tools/meson.ML	Tue Sep 29 18:14:08 2009 +0200
@@ -319,7 +319,7 @@
   Strips universal quantifiers and breaks up conjunctions.
   Eliminates existential quantifiers using skoths: Skolemization theorems.*)
 fun cnf skoths ctxt (th,ths) =
-  let val ctxtr = ref ctxt
+  let val ctxtr = Unsynchronized.ref ctxt
       fun cnf_aux (th,ths) =
         if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
         else if not (has_conns ["All","Ex","op &"] (prop_of th))