# HG changeset patch
# User wenzelm
# Date 1191942641 -7200
# Node ID 408becab067e7156d69b983e45803db4e532cba1
# Parent  3419943838f549472cc49f57de4855eac8602b7d
renamed AxClass.get_definition to AxClass.get_info (again);
AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;

diff -r 3419943838f5 -r 408becab067e src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Oct 09 17:10:38 2007 +0200
+++ b/src/Pure/axclass.ML	Tue Oct 09 17:10:41 2007 +0200
@@ -18,7 +18,7 @@
   val add_arity: thm -> theory -> theory
   val prove_classrel: class * class -> tactic -> theory -> theory
   val prove_arity: string * sort list * sort -> tactic -> theory -> theory
-  val get_definition: theory -> class -> {def: thm, intro: thm, axioms: thm list,
+  val get_info: theory -> class -> {def: thm, intro: thm, axioms: thm list,
     params: (string * typ) list}
   val class_intros: theory -> thm list
   val class_of_param: theory -> string -> class option
@@ -26,15 +26,15 @@
   val print_axclasses: theory -> unit
   val cert_classrel: theory -> class * class -> class * class
   val read_classrel: theory -> xstring * xstring -> class * class
-  val axiomatize_class: bstring * xstring list -> theory -> theory
-  val axiomatize_class_i: bstring * class list -> theory -> theory
-  val axiomatize_classrel: (xstring * xstring) list -> theory -> theory
-  val axiomatize_classrel_i: (class * class) list -> theory -> theory
-  val axiomatize_arity: xstring * string list * string -> theory -> theory
-  val axiomatize_arity_i: arity -> theory -> theory
+  val axiomatize_class: bstring * class list -> theory -> theory
+  val axiomatize_class_cmd: bstring * xstring list -> theory -> theory
+  val axiomatize_classrel: (class * class) list -> theory -> theory
+  val axiomatize_classrel_cmd: (xstring * xstring) list -> theory -> theory
+  val axiomatize_arity: arity -> theory -> theory
+  val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
   type cache
+  val of_sort: theory -> typ * sort -> cache -> thm list * cache  (*exception Sorts.CLASS_ERROR*)
   val cache: cache
-  val of_sort: theory -> typ * sort -> cache -> thm list * cache  (*exception Sorts.CLASS_ERROR*)
 end;
 
 structure AxClass: AX_CLASS =
@@ -113,7 +113,7 @@
 
 val lookup_def = Symtab.lookup o #1 o get_axclasses;
 
-fun get_definition thy c =
+fun get_info thy c =
   (case lookup_def thy c of
     SOME (AxClass info) => info
   | NONE => error ("No such axclass: " ^ quote c));
@@ -136,7 +136,7 @@
 fun class_of_param thy =
   AList.lookup (op =) (#2 (get_axclasses thy));
 
-fun params_of_class thy class = (Name.aT, #params (get_definition thy class));
+fun params_of_class thy class = (Name.aT, #params (get_info thy class));
 
 
 (* maintain instances *)
@@ -156,7 +156,7 @@
 
 
 fun the_arity thy a (c, Ss) =
-  (case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss)  of
+  (case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss) of
     SOME th => Thm.transfer thy th
   | NONE => error ("Unproven type arity " ^
       Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
@@ -389,7 +389,7 @@
     |-> (fn cs => mk_axioms cs
     #-> (fn axioms_prop => define_class (name, superclasses)
            (map fst cs @ other_consts) axioms_prop
-    #-> (fn class => `(fn thy => get_definition thy class)
+    #-> (fn class => `(fn thy => get_info thy class)
     #-> (fn {axioms, ...} => fold (add_constraint class) cs
     #> pair (class, (cs, axioms))))))
   end;
@@ -431,12 +431,12 @@
 
 in
 
-val axiomatize_class = ax_class Sign.read_class read_classrel;
-val axiomatize_class_i = ax_class Sign.certify_class cert_classrel;
-val axiomatize_classrel = ax_classrel read_classrel;
-val axiomatize_classrel_i = ax_classrel cert_classrel;
-val axiomatize_arity = ax_arity Sign.read_arity;
-val axiomatize_arity_i = ax_arity Sign.cert_arity;
+val axiomatize_class = ax_class Sign.certify_class cert_classrel;
+val axiomatize_class_cmd = ax_class Sign.read_class read_classrel;
+val axiomatize_classrel = ax_classrel cert_classrel;
+val axiomatize_classrel_cmd = ax_classrel read_classrel;
+val axiomatize_arity = ax_arity Sign.cert_arity;
+val axiomatize_arity_cmd = ax_arity Sign.read_arity;
 
 end;
 
@@ -445,7 +445,6 @@
 (** explicit derivations -- cached **)
 
 datatype cache = Types of (class * thm) list Typtab.table;
-val cache = Types Typtab.empty;
 
 local
 
@@ -490,4 +489,6 @@
 
 end;
 
+val cache = Types Typtab.empty;
+
 end;