src/HOL/Tools/meson.ML
changeset 32740 9dd0a2f83429
parent 32283 3bebc195c124
child 32955 4a78daeb012b
     1.1 --- a/src/HOL/Tools/meson.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -319,7 +319,7 @@
     1.4    Strips universal quantifiers and breaks up conjunctions.
     1.5    Eliminates existential quantifiers using skoths: Skolemization theorems.*)
     1.6  fun cnf skoths ctxt (th,ths) =
     1.7 -  let val ctxtr = ref ctxt
     1.8 +  let val ctxtr = Unsynchronized.ref ctxt
     1.9        fun cnf_aux (th,ths) =
    1.10          if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
    1.11          else if not (has_conns ["All","Ex","op &"] (prop_of th))