src/HOL/Tools/typedef_package.ML

     val typedef_deps = Term.fold_aterms (fn Const c => insert (op =) c | _ => I) set' [];
 
     fun add_def eq thy =
       if def then
         thy
-        |> PureThy.add_defs_i false [Thm.no_attributes eq]
+        |> PureThy.add_defs false [Thm.no_attributes eq]
         |-> (fn [th] => pair (SOME th))
       else (NONE, thy);
 
     fun typedef_result nonempty =
       ObjectLogic.typedecl (t, vs, mx)

       #> Sign.add_consts_i
        ((if def then [(name, setT', NoSyn)] else []) @
         [(Rep_name, newT --> oldT, NoSyn),
          (Abs_name, oldT --> newT, NoSyn)])
       #> add_def (PrimitiveDefs.mk_defpair (setC, set))
-      ##>> PureThy.add_axioms_i [((typedef_name, typedef_prop),
+      ##>> PureThy.add_axioms [((typedef_name, typedef_prop),
           [apsnd (fn cond_axm => nonempty RS cond_axm)])]
       ##> Theory.add_deps "" (dest_Const RepC) typedef_deps
       ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps
       #-> (fn (set_def, [type_definition]) => fn thy1 =>
         let