# HG changeset patch
# User wenzelm
# Date 1399907852 -7200
# Node ID 952833323c997ca5a1db01dbd4eed7e77fabace6
# Parent  35ce6dab3f5ef20072e9f0a4a42d470d9447270a
tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";

diff -r 35ce6dab3f5e -r 952833323c99 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon May 12 00:13:38 2014 +0200
+++ b/src/HOL/HOL.thy	Mon May 12 17:17:32 2014 +0200
@@ -44,7 +44,7 @@
 
 subsubsection {* Core syntax *}
 
-setup {* Axclass.axiomatize_class (@{binding type}, []) *}
+setup {* Axclass.class_axiomatization (@{binding type}, []) *}
 default_sort type
 setup {* Object_Logic.add_base_sort @{sort type} *}
 
diff -r 35ce6dab3f5e -r 952833323c99 src/HOL/HOLCF/Tools/Domain/domain.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Mon May 12 00:13:38 2014 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Mon May 12 17:17:32 2014 +0200
@@ -44,7 +44,7 @@
 fun add_arity ((b, sorts, mx), sort) thy : theory =
   thy
   |> Sign.add_types_global [(b, length sorts, mx)]
-  |> Axclass.axiomatize_arity (Sign.full_name thy b, sorts, sort)
+  |> Axclass.arity_axiomatization (Sign.full_name thy b, sorts, sort)
 
 fun gen_add_domain
     (prep_sort : theory -> 'a -> sort)
diff -r 35ce6dab3f5e -r 952833323c99 src/HOL/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Mon May 12 00:13:38 2014 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Mon May 12 17:17:32 2014 +0200
@@ -104,7 +104,7 @@
     fun thy_arity (_, _, (lhsT, _)) =
         let val (dname, tvars) = dest_Type lhsT
         in (dname, map (snd o dest_TFree) tvars, @{sort pcpo}) end
-    val thy = fold (Axclass.axiomatize_arity o thy_arity) dom_eqns thy
+    val thy = fold (Axclass.arity_axiomatization o thy_arity) dom_eqns thy
 
     (* declare and axiomatize abs/rep *)
     val (iso_infos, thy) =
diff -r 35ce6dab3f5e -r 952833323c99 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon May 12 00:13:38 2014 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon May 12 17:17:32 2014 +0200
@@ -428,7 +428,7 @@
         fun arity (vs, tbind, _, _, _) =
           (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"})
       in
-        fold Axclass.axiomatize_arity (map arity doms) tmp_thy
+        fold Axclass.arity_axiomatization (map arity doms) tmp_thy
       end
 
     (* check bifiniteness of right-hand sides *)
diff -r 35ce6dab3f5e -r 952833323c99 src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Mon May 12 00:13:38 2014 +0200
+++ b/src/Pure/Isar/typedecl.ML	Mon May 12 17:17:32 2014 +0200
@@ -29,7 +29,7 @@
 fun object_logic_arity name thy =
   (case Object_Logic.get_base_sort thy of
     NONE => thy
-  | SOME S => Axclass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy);
+  | SOME S => Axclass.arity_axiomatization (name, replicate (Sign.arity_number thy name) S, S) thy);
 
 fun basic_decl decl (b, n, mx) lthy =
   let val name = Local_Theory.full_name lthy b in
diff -r 35ce6dab3f5e -r 952833323c99 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon May 12 00:13:38 2014 +0200
+++ b/src/Pure/axclass.ML	Mon May 12 17:17:32 2014 +0200
@@ -30,9 +30,9 @@
   val prove_arity: string * sort list * sort -> (Proof.context -> tactic) -> theory -> theory
   val define_class: binding * class list -> string list ->
     (Thm.binding * term list) list -> theory -> class * theory
-  val axiomatize_classrel: (class * class) list -> theory -> theory
-  val axiomatize_arity: arity -> theory -> theory
-  val axiomatize_class: binding * class list -> theory -> theory
+  val classrel_axiomatization: (class * class) list -> theory -> theory
+  val arity_axiomatization: arity -> theory -> theory
+  val class_axiomatization: binding * class list -> theory -> theory
 end;
 
 structure Axclass: AXCLASS =
@@ -582,7 +582,7 @@
 local
 
 (*old-style axioms*)
-fun axiomatize prep mk name add raw_args thy =
+fun add_axioms prep mk name add raw_args thy =
   let
     val args = prep thy raw_args;
     val specs = mk args;
@@ -598,22 +598,22 @@
 
 in
 
-val axiomatize_classrel =
-  axiomatize (map o cert_classrel) (map Logic.mk_classrel)
+val classrel_axiomatization =
+  add_axioms (map o cert_classrel) (map Logic.mk_classrel)
     (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
 
-val axiomatize_arity =
-  axiomatize (Proof_Context.cert_arity o Proof_Context.init_global) Logic.mk_arities
+val arity_axiomatization =
+  add_axioms (Proof_Context.cert_arity o Proof_Context.init_global) Logic.mk_arities
     (map (prefix arity_prefix) o Logic.name_arities) add_arity;
 
-fun axiomatize_class (bclass, raw_super) thy =
+fun class_axiomatization (bclass, raw_super) thy =
   let
     val class = Sign.full_name thy bclass;
     val super = map (Sign.certify_class thy) raw_super |> Sign.minimize_sort thy;
   in
     thy
     |> Sign.primitive_class (bclass, super)
-    |> axiomatize_classrel (map (fn c => (class, c)) super)
+    |> classrel_axiomatization (map (fn c => (class, c)) super)
     |> Theory.add_deps_global "" (class_const class) (map class_const super)
   end;