TFL/tfl.ML

                  (name, Ty, S.list_mk_abs (args,rhs))
      val ([def0], theory) =
        thy
        |> PureThy.add_defs_i false
             [Thm.no_attributes (fid ^ "_def", defn)]
-     val def = freezeT 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))  *)
      val tych = Thry.typecheck theory
      val full_rqt_prop = map (Dcterm.mk_prop o tych) full_rqt