src/Pure/axclass.ML

     (class * ((string * typ) list * thm list)) * theory
   val add_classrel: thm -> theory -> theory
   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
   val params_of_class: theory -> class -> string * (string * typ) list
   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 =
 struct
 

 val get_axclasses = #1 o AxClassData.get;
 fun map_axclasses f = AxClassData.map (apfst f);
 
 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));
 
 fun class_intros thy =

 fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c]));
 
 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 *)
 
 val get_instances = #2 o AxClassData.get;

 fun put_classrel arg = map_instances (fn (classrel, arities) =>
   (insert (eq_fst op =) arg classrel, arities));
 
 
 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])));
 
 fun put_arity ((t, Ss, c), th) = map_instances (fn (classrel, arities) =>

     |> fold_map add_const consts
     ||> Sign.restore_naming thy
     |-> (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;
 
 

     |> Theory.add_deps "" (class_const class) (map class_const super)
   end;
 
 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;
 
 
 
 (** explicit derivations -- cached **)
 
 datatype cache = Types of (class * thm) list Typtab.table;
-val cache = Types Typtab.empty;
 
 local
 
 fun lookup_type (Types cache) = AList.lookup (op =) o Typtab.lookup_list cache;
 fun insert_type T der (Types cache) = Types (Typtab.insert_list (eq_fst op =) (T, der) cache);

         |> Thm.adjust_maxidx_thm ~1);
   in (ths, cache') end;
 
 end;
 
+val cache = Types Typtab.empty;
+
 end;