src/HOL/Tools/inductive_realizer.ML

       (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss);
 
     val thy1' = thy1 |>
       Theory.copy |>
       Sign.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
-      fold (fn s => AxClass.axiomatize_arity_i
+      fold (fn s => AxClass.axiomatize_arity
         (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
         Extraction.add_typeof_eqns_i ty_eqs;
     val dts = List.mapPartial (fn (s, rs) => if s mem rsets then
       SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;