# HG changeset patch
# User wenzelm
# Date 1272912829 -7200
# Node ID 712724c32ac80bf047b94c7a2fcba022bdd9e0bd
# Parent  88756a5a92fc8cfc7d88bd0d08863ca2864f5f91
replaced Thm.legacy_freezeT by Thm.unvarify_global -- these facts stem from closed definitions, i.e. there are no term Vars;

diff -r 88756a5a92fc -r 712724c32ac8 src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Mon May 03 20:13:36 2010 +0200
+++ b/src/HOL/Tools/TFL/post.ML	Mon May 03 20:53:49 2010 +0200
@@ -141,7 +141,7 @@
 fun simplify_defn strict thy cs ss congs wfs id pats def0 =
    let
        val ctxt = ProofContext.init_global thy
-       val def = Thm.legacy_freezeT def0 RS meta_eq_to_obj_eq
+       val def = Thm.unvarify_global def0 RS meta_eq_to_obj_eq
        val {rules,rows,TCs,full_pats_TCs} =
            Prim.post_definition congs (thy, (def,pats))
        val {lhs=f,rhs} = S.dest_eq (concl def)
diff -r 88756a5a92fc -r 712724c32ac8 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Mon May 03 20:13:36 2010 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Mon May 03 20:53:49 2010 +0200
@@ -541,7 +541,7 @@
        thy
        |> PureThy.add_defs false
             [Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
-     val def = Thm.legacy_freezeT def0;
+     val def = Thm.unvarify_global def0;
      val dummy =
        if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def)
        else ()