src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

           (Predicate_Comp_Funs.mk_Enum (HOLogic.tupled_lambda (HOLogic.mk_tuple outargs)
             (list_comb (Const (name, T), args))))
         val lhs = Const (mode_cname, funT)
         val def = Logic.mk_equals (lhs, predterm)
         val ([definition], thy') = thy |>
-          Sign.add_consts_i [(Binding.name mode_cbasename, funT, NoSyn)] |>
+          Sign.add_consts [(Binding.name mode_cbasename, funT, NoSyn)] |>
           Global_Theory.add_defs false [((Binding.name (Thm.def_name mode_cbasename), def), [])]
         val ctxt' = Proof_Context.init_global thy'
         val rules as ((intro, elim), _) =
           create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T))
         in

       let
         val function_name_prefix = Comp_Mod.function_name_prefix comp_modifiers
         val mode_cname = create_constname_of_mode options thy function_name_prefix name T mode
         val funT = Comp_Mod.funT_of comp_modifiers mode T
       in
-        thy |> Sign.add_consts_i [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
+        thy |> Sign.add_consts [(Binding.name (Long_Name.base_name mode_cname), funT, NoSyn)]
         |> set_function_name (Comp_Mod.compilation comp_modifiers) name mode mode_cname
       end;
   in
     thy
     |> defined_function_of (Comp_Mod.compilation comp_modifiers) name