1.1 --- a/src/HOL/SMT/Tools/smt_normalize.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/SMT/Tools/smt_normalize.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -304,11 +304,11 @@
     1.4  fun lift_lambdas ctxt thms =
     1.5    let
     1.6      val declare_frees = fold (Thm.fold_terms Term.declare_term_frees)
     1.7 -    val names = ref (declare_frees thms (Name.make_context []))
     1.8 -    val fresh_name = change_result names o yield_singleton Name.variants
     1.9 +    val names = Unsynchronized.ref (declare_frees thms (Name.make_context []))
    1.10 +    val fresh_name = Unsynchronized.change_result names o yield_singleton Name.variants
    1.11  
    1.12 -    val defs = ref (Termtab.empty : (int * thm) Termtab.table)
    1.13 -    fun add_def t thm = change defs (Termtab.update (t, (serial (), thm)))
    1.14 +    val defs = Unsynchronized.ref (Termtab.empty : (int * thm) Termtab.table)
    1.15 +    fun add_def t thm = Unsynchronized.change defs (Termtab.update (t, (serial (), thm)))
    1.16      fun make_def cvs eq = Thm.symmetric (fold norm_meta_def cvs eq)
    1.17      fun def_conv cvs ctxt ct =
    1.18        let