src/HOL/Tools/Function/size.ML

         val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
       in (thm', lthy') end;
 
     val ((size_def_thms, size_def_thms'), thy') =
       thy
-      |> Sign.add_consts_i (map (fn (s, T) =>
+      |> Sign.add_consts (map (fn (s, T) =>
            (Binding.name (Long_Name.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
            (size_names ~~ recTs1))
       |> Global_Theory.add_defs false
         (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
            (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))