# HG changeset patch
# User wenzelm
# Date 1140643116 -3600
# Node ID a278d1e65c1de5dada8f9e1bd62810451479a4cb
# Parent  e1b6a50713489f4779e4188e2f36bd8efb61baa5
renamed class_axms to class_intros;

diff -r e1b6a5071348 -r a278d1e65c1d src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Wed Feb 22 22:18:33 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Wed Feb 22 22:18:36 2006 +0100
@@ -268,12 +268,12 @@
 
 (* tactics and methods *)
 
-fun class_loc_axms thy =
-  AxClass.class_axms thy @ the_intros thy;
+fun class_intros thy =
+  AxClass.class_intros thy @ the_intros thy;
 
 fun intro_classes_tac facts st =
   (ALLGOALS (Method.insert_tac facts THEN'
-      REPEAT_ALL_NEW (resolve_tac (class_loc_axms (Thm.theory_of_thm st))))
+      REPEAT_ALL_NEW (resolve_tac (class_intros (Thm.theory_of_thm st))))
     THEN Tactic.distinct_subgoals_tac) st;
 
 fun default_intro_classes_tac [] = intro_classes_tac []
diff -r e1b6a5071348 -r a278d1e65c1d src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Feb 22 22:18:33 2006 +0100
+++ b/src/Pure/axclass.ML	Wed Feb 22 22:18:36 2006 +0100
@@ -18,15 +18,17 @@
   val add_arity_thms: thm list -> theory -> theory
   val add_inst_subclass: xstring * xstring -> tactic -> theory -> theory
   val add_inst_subclass_i: class * class -> tactic -> theory -> theory
-  val add_inst_arity: (theory -> theory) -> xstring * string list * string -> tactic -> theory -> theory
-  val add_inst_arity_i: (theory -> theory) -> string * sort list * sort -> tactic -> theory -> theory
+  val add_inst_arity: (theory -> theory) ->
+    xstring * string list * string -> tactic -> theory -> theory
+  val add_inst_arity_i: (theory -> theory) ->
+    string * sort list * sort -> tactic -> theory -> theory
   val instance_subclass: xstring * xstring -> theory -> Proof.state
   val instance_subclass_i: class * class -> theory -> Proof.state
   val instance_arity: (theory -> theory) -> xstring * string list * string -> theory -> Proof.state
   val instance_arity_i: (theory -> theory) -> string * sort list * sort -> theory -> Proof.state
   val read_arity: theory -> xstring * string list * string -> arity
   val cert_arity: theory -> string * sort list * sort -> arity
-  val class_axms: theory -> thm list
+  val class_intros: theory -> thm list
 end;
 
 structure AxClass: AX_CLASS =
@@ -146,8 +148,7 @@
     NONE => error ("Unknown axclass " ^ quote c)
   | SOME info => info);
 
-
-fun class_axms thy =
+fun class_intros thy =
   let val classes = Sign.classes thy in
     map (Thm.class_triv thy) classes @
     List.mapPartial (Option.map #intro o lookup_info thy) classes