TFL/tfl.ML

--- a/TFL/tfl.ML	Mon Jun 19 19:56:32 2006 +0200
+++ b/TFL/tfl.ML	Mon Jun 19 20:21:30 2006 +0200
@@ -555,7 +555,7 @@
        thy
        |> PureThy.add_defs_i false
             [Thm.no_attributes (fid ^ "_def", defn)]
-     val def = Thm.freezeT def0;
+     val ([def], _) = Variable.importT [def0] (Variable.thm_context def0);
      val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
                            else ()
      (* val fconst = #lhs(S.dest_eq(concl def))  *)