replaced Thm.legacy_freezeT by Thm.unvarify_global -- these facts stem from closed definitions, i.e. there are no term Vars;

--- 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)

--- 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 ()