changeset 19927 | 9286e99b2808 |
parent 19925 | 3f9341831812 |
child 20062 | 60de4603e645 |
--- a/TFL/tfl.ML Mon Jun 19 20:21:32 2006 +0200 +++ b/TFL/tfl.ML Mon Jun 19 22:06:36 2006 +0200 @@ -555,7 +555,7 @@ thy |> PureThy.add_defs_i false [Thm.no_attributes (fid ^ "_def", defn)] - val ([def], _) = Variable.importT [def0] (Variable.thm_context def0); + val def = Thm.freezeT def0; val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def) else () (* val fconst = #lhs(S.dest_eq(concl def)) *)