diff -r 24738db98d34 -r ce171cbd4b93 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -392,7 +392,7 @@
                           (wfrec $ map_types poly_tvars R)
                       $ functional
      val def_term = mk_const_def thy (x, Ty, wfrec_R_M)
-     val ([def], thy') = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy
+     val ([def], thy') = PureThy.add_defs false [Thm.no_attributes (def_name, def_term)] thy
  in (thy', def) end;
 end;
 
@@ -550,7 +550,7 @@
      val defn = mk_const_def thy (name, Ty, S.list_mk_abs (args,rhs))
      val ([def0], theory) =
        thy
-       |> PureThy.add_defs_i false
+       |> PureThy.add_defs false
             [Thm.no_attributes (fid ^ "_def", defn)]
      val def = Thm.freezeT def0;
      val dummy = if !trace then writeln ("DEF = " ^ Display.string_of_thm def)