# HG changeset patch
# User wenzelm
# Date 1191942634 -7200
# Node ID bcb6b098df115bee0c42bb4414a1f77c79d67417
# Parent  f38dd8d0a30df2e25489af1898a93c7ac9611e4b
AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;

diff -r f38dd8d0a30d -r bcb6b098df11 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Oct 09 17:10:32 2007 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Oct 09 17:10:34 2007 +0200
@@ -300,7 +300,7 @@
     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
diff -r f38dd8d0a30d -r bcb6b098df11 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Tue Oct 09 17:10:32 2007 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Tue Oct 09 17:10:34 2007 +0200
@@ -48,7 +48,7 @@
 (** type declarations **)
 
 fun HOL_arity (raw_name, args, mx) thy =
-  thy |> AxClass.axiomatize_arity_i
+  thy |> AxClass.axiomatize_arity
     (Sign.full_name thy (Syntax.type_name raw_name mx),
       replicate (length args) HOLogic.typeS, HOLogic.typeS);
 
diff -r f38dd8d0a30d -r bcb6b098df11 src/HOLCF/Tools/domain/domain_extender.ML
--- a/src/HOLCF/Tools/domain/domain_extender.ML	Tue Oct 09 17:10:32 2007 +0200
+++ b/src/HOLCF/Tools/domain/domain_extender.ML	Tue Oct 09 17:10:34 2007 +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''' |> Sign.add_types     (map thy_type  dtnvs)
-		       |> fold (AxClass.axiomatize_arity_i o thy_arity) dtnvs;
+		       |> fold (AxClass.axiomatize_arity 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');