src/HOL/Tools/inductive_realizer.ML

       (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs rs) rss);
 
     val thy1' = thy1 |>
       Theory.copy |>
       Theory.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
-      Theory.add_arities_i (map (fn s =>
-        (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames) |>
+      fold (fn s => AxClass.axiomatize_arity_i
+        (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 rs) else NONE) rss;
 
     (** datatype representing computational content of inductive set **)