AxClass.axiomatize_arity_i;

--- a/src/HOL/Tools/inductive_realizer.ML	Sun Apr 30 22:50:01 2006 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Sun Apr 30 22:50:03 2006 +0200
@@ -308,8 +308,8 @@
     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;

--- a/src/HOL/Tools/typedef_package.ML	Sun Apr 30 22:50:01 2006 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Sun Apr 30 22:50:03 2006 +0200
@@ -50,16 +50,15 @@
 
 (** type declarations **)
 
+fun HOL_arity (raw_name, args, mx) thy =
+  thy |> AxClass.axiomatize_arity_i
+    (Sign.full_name thy (Syntax.type_name raw_name mx),
+      replicate (length args) HOLogic.typeS, HOLogic.typeS);
+
 fun add_typedecls decls thy =
-  let
-    fun arity_of (raw_name, args, mx) =
-      (Sign.full_name thy (Syntax.type_name raw_name mx),
-        replicate (length args) HOLogic.typeS, HOLogic.typeS);
-  in
-    thy
-    |> Theory.add_typedecls decls
-    |> can (Theory.assert_super HOL.thy) ? Theory.add_arities_i (map arity_of decls)
-  end;
+  thy
+  |> Theory.add_typedecls decls
+  |> can (Theory.assert_super HOL.thy) ? fold HOL_arity decls;
 
 
 

--- a/src/HOLCF/domain/extender.ML	Sun Apr 30 22:50:01 2006 +0200
+++ b/src/HOLCF/domain/extender.ML	Sun Apr 30 22:50:03 2006 +0200
@@ -106,7 +106,7 @@
     fun thy_type  (dname,tvars)  = (Sign.base_name dname, length tvars, NoSyn);
     fun thy_arity (dname,tvars)  = (dname, map (snd o dest_TFree) tvars, pcpoS);
     val thy'' = thy''' |> Theory.add_types     (map thy_type  dtnvs)
-		       |> Theory.add_arities_i (map thy_arity dtnvs);
+		       |> fold (AxClass.axiomatize_arity_i o thy_arity) dtnvs;
     val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons''';
     val eqs' = check_and_sort_domain (dtnvs,cons'') thy'';
     val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');