src/HOL/Tools/function_package/size.ML

--- a/src/HOL/Tools/function_package/size.ML	Tue Jul 29 08:15:39 2008 +0200
+++ b/src/HOL/Tools/function_package/size.ML	Tue Jul 29 08:15:40 2008 +0200
@@ -143,7 +143,7 @@
       |> Sign.add_consts_i (map (fn (s, T) =>
            (Sign.base_name s, param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
            (size_names ~~ recTs1))
-      |> PureThy.add_defs_i false
+      |> PureThy.add_defs false
         (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
            (def_names ~~ (size_fns ~~ rec_combs1)))
       ||> TheoryTarget.instantiation