src/Pure/axclass.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18754 4e41252eae57
--- a/src/Pure/axclass.ML	Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/axclass.ML	Sat Jan 21 23:02:14 2006 +0100
@@ -12,7 +12,7 @@
   val get_info: theory -> string -> {super_classes: class list, intro: thm, axioms: thm list}
   val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list ->
     theory -> {intro: thm, axioms: thm list} * theory
-  val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list ->
+  val add_axclass_i: bstring * class list -> ((bstring * term) * attribute list) list ->
     theory -> {intro: thm, axioms: thm list} * theory
   val add_classrel_thms: thm list -> theory -> theory
   val add_arity_thms: thm list -> theory -> theory
@@ -216,7 +216,7 @@
 
 in
 
-val add_axclass = ext_axclass Sign.intern_class Theory.read_axm Attrib.global_attribute;
+val add_axclass = ext_axclass Sign.intern_class Theory.read_axm Attrib.attribute;
 val add_axclass_i = ext_axclass (K I) Theory.cert_axm (K I);
 
 end;