# HG changeset patch
# User haftmann
# Date 1266916272 -3600
# Node ID fbdc860d87a37bb70a663607df3bb5dabba1c47b
# Parent  8fd9d555d04dbb2f0acfe8407c9593367ac061f8
dropped axclass

diff -r 8fd9d555d04d -r fbdc860d87a3 src/HOL/Algebra/abstract/Ideal2.thy
--- a/src/HOL/Algebra/abstract/Ideal2.thy	Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ideal2.thy	Tue Feb 23 10:11:12 2010 +0100
@@ -1,6 +1,5 @@
 (*
     Ideals for commutative rings
-    $Id$
     Author: Clemens Ballarin, started 24 September 1999
 *)
 
@@ -23,9 +22,8 @@
 
 text {* Principle ideal domains *}
 
-axclass pid < "domain"
-  pid_ax: "is_ideal I ==> is_pideal I"
-
+class pid =
+  assumes pid_ax: "is_ideal (I :: 'a::domain \<Rightarrow> _) \<Longrightarrow> is_pideal I"
 
 (* is_ideal *)
 
diff -r 8fd9d555d04d -r fbdc860d87a3 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/Bali/Decl.thy	Tue Feb 23 10:11:12 2010 +0100
@@ -230,18 +230,22 @@
 
 datatype memberid = fid vname | mid sig
 
-axclass has_memberid < "type"
-consts
- memberid :: "'a::has_memberid \<Rightarrow> memberid"
+class has_memberid =
+  fixes memberid :: "'a \<Rightarrow> memberid"
 
-instance memberdecl::has_memberid ..
+instantiation memberdecl :: has_memberid
+begin
 
-defs (overloaded)
+definition
 memberdecl_memberid_def:
   "memberid m \<equiv> (case m of
                     fdecl (vn,f)  \<Rightarrow> fid vn
                   | mdecl (sig,m) \<Rightarrow> mid sig)"
 
+instance ..
+
+end
+
 lemma memberid_fdecl_simp[simp]: "memberid (fdecl (vn,f)) = fid vn"
 by (simp add: memberdecl_memberid_def)
 
@@ -254,12 +258,17 @@
 lemma memberid_mdecl_simp1: "memberid (mdecl m) = mid (fst m)"
 by (cases m) (simp add: memberdecl_memberid_def)
 
-instance * :: (type, has_memberid) has_memberid ..
+instantiation * :: (type, has_memberid) has_memberid
+begin
 
-defs (overloaded)
+definition
 pair_memberid_def:
   "memberid p \<equiv> memberid (snd p)"
 
+instance ..
+
+end
+
 lemma memberid_pair_simp[simp]: "memberid (c,m) = memberid m"
 by (simp add: pair_memberid_def)
 
diff -r 8fd9d555d04d -r fbdc860d87a3 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy	Tue Feb 23 10:11:12 2010 +0100
@@ -79,41 +79,60 @@
 text {* overloaded selector @{text accmodi} to select the access modifier 
 out of various HOL types *}
 
-axclass has_accmodi < "type"
-consts accmodi:: "'a::has_accmodi \<Rightarrow> acc_modi"
+class has_accmodi =
+  fixes accmodi:: "'a \<Rightarrow> acc_modi"
+
+instantiation acc_modi :: has_accmodi
+begin
 
-instance acc_modi::has_accmodi ..
+definition
+  acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
 
-defs (overloaded)
-acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
+instance ..
+
+end
 
 lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a"
 by (simp add: acc_modi_accmodi_def)
 
-instance decl_ext_type:: ("type") has_accmodi ..
+instantiation decl_ext_type:: (type) has_accmodi
+begin
 
-defs (overloaded)
-decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
+definition
+  decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
 
+instance ..
+
+end
 
 lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d"
 by (simp add: decl_acc_modi_def)
 
-instance * :: ("type",has_accmodi) has_accmodi ..
+instantiation * :: (type, has_accmodi) has_accmodi
+begin
 
-defs (overloaded)
-pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
+definition
+  pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
+
+instance ..
+
+end
 
 lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)"
 by (simp add: pair_acc_modi_def)
 
-instance memberdecl :: has_accmodi ..
+instantiation memberdecl :: has_accmodi
+begin
 
-defs (overloaded)
-memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
+definition
+  memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
                                           fdecl f \<Rightarrow> accmodi f
                                         | mdecl m \<Rightarrow> accmodi m)"
 
+instance ..
+
+end
+
 lemma memberdecl_fdecl_acc_modi_simp[simp]:
  "accmodi (fdecl m) = accmodi m"
 by (simp add: memberdecl_acc_modi_def)
@@ -125,21 +144,35 @@
 text {* overloaded selector @{text declclass} to select the declaring class 
 out of various HOL types *}
 
-axclass has_declclass < "type"
-consts declclass:: "'a::has_declclass \<Rightarrow> qtname"
+class has_declclass =
+  fixes declclass:: "'a \<Rightarrow> qtname"
+
+instantiation qtname_ext_type :: (type) has_declclass
+begin
 
-instance qtname_ext_type::("type") has_declclass ..
+definition
+  "declclass q \<equiv> \<lparr> pid = pid q, tid = tid q \<rparr>"
+
+instance ..
 
-defs (overloaded)
-qtname_declclass_def: "declclass (q::qtname) \<equiv> q"
+end
+
+lemma qtname_declclass_def:
+  "declclass q \<equiv> (q::qtname)"
+  by (induct q) (simp add: declclass_qtname_ext_type_def)
 
 lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
 by (simp add: qtname_declclass_def)
 
-instance * :: ("has_declclass","type") has_declclass ..
+instantiation * :: (has_declclass, type) has_declclass
+begin
 
-defs (overloaded)
-pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
+definition
+  pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
+
+instance ..
+
+end
 
 lemma pair_declclass_simp[simp]: "declclass (c,x) = declclass c" 
 by (simp add: pair_declclass_def)
@@ -147,25 +180,38 @@
 text {* overloaded selector @{text is_static} to select the static modifier 
 out of various HOL types *}
 
+class has_static =
+  fixes is_static :: "'a \<Rightarrow> bool"
 
-axclass has_static < "type"
-consts is_static :: "'a::has_static \<Rightarrow> bool"
+instantiation decl_ext_type :: (has_static) has_static
+begin
 
-instance decl_ext_type :: ("has_static") has_static ..
+instance ..
+
+end
 
-instance member_ext_type :: ("type") has_static ..
+instantiation member_ext_type :: (type) has_static
+begin
+
+instance ..
 
-defs (overloaded)
-static_field_type_is_static_def: 
- "is_static (m::('b member_scheme)) \<equiv> static m"
+end
+
+axiomatization where
+  static_field_type_is_static_def: "is_static (m::('a member_scheme)) \<equiv> static m"
 
 lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
 by (simp add: static_field_type_is_static_def)
 
-instance * :: ("type","has_static") has_static ..
+instantiation * :: (type, has_static) has_static
+begin
 
-defs (overloaded)
-pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
+definition
+  pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
+
+instance ..
+
+end
 
 lemma pair_is_static_simp [simp]: "is_static (x,s) = is_static s"
 by (simp add: pair_is_static_def)
@@ -173,14 +219,19 @@
 lemma pair_is_static_simp1: "is_static p = is_static (snd p)"
 by (simp add: pair_is_static_def)
 
-instance memberdecl:: has_static ..
+instantiation memberdecl :: has_static
+begin
 
-defs (overloaded)
+definition
 memberdecl_is_static_def: 
  "is_static m \<equiv> (case m of
                     fdecl f \<Rightarrow> is_static f
                   | mdecl m \<Rightarrow> is_static m)"
 
+instance ..
+
+end
+
 lemma memberdecl_is_static_fdecl_simp[simp]:
  "is_static (fdecl f) = is_static f"
 by (simp add: memberdecl_is_static_def)
@@ -389,18 +440,32 @@
 text {* overloaded selector @{text resTy} to select the result type 
 out of various HOL types *}
 
-axclass has_resTy < "type"
-consts resTy:: "'a::has_resTy \<Rightarrow> ty"
+class has_resTy =
+  fixes resTy:: "'a \<Rightarrow> ty"
+
+instantiation decl_ext_type :: (has_resTy) has_resTy
+begin
 
-instance decl_ext_type :: ("has_resTy") has_resTy ..
+instance ..
+
+end
+
+instantiation member_ext_type :: (has_resTy) has_resTy
+begin
 
-instance member_ext_type :: ("has_resTy") has_resTy ..
+instance ..
 
-instance mhead_ext_type :: ("type") has_resTy ..
+end
+
+instantiation mhead_ext_type :: (type) has_resTy
+begin
 
-defs (overloaded)
-mhead_ext_type_resTy_def: 
- "resTy (m::('b mhead_scheme)) \<equiv> resT m"
+instance ..
+
+end
+
+axiomatization where
+  mhead_ext_type_resTy_def: "resTy (m::('b mhead_scheme)) \<equiv> resT m"
 
 lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m"
 by (simp add: mhead_ext_type_resTy_def)
@@ -408,10 +473,15 @@
 lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
 by (simp add: mhead_def mhead_resTy_simp)
 
-instance * :: ("type","has_resTy") has_resTy ..
+instantiation * :: ("type","has_resTy") has_resTy
+begin
 
-defs (overloaded)
-pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
+definition
+  pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
+
+instance ..
+
+end
 
 lemma pair_resTy_simp[simp]: "resTy (x,m) = resTy m"
 by (simp add: pair_resTy_def)
diff -r 8fd9d555d04d -r fbdc860d87a3 src/HOL/Bali/Name.thy
--- a/src/HOL/Bali/Name.thy	Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/Bali/Name.thy	Tue Feb 23 10:11:12 2010 +0100
@@ -48,29 +48,34 @@
           pid :: pname  
           tid :: tname
 
-axclass has_pname < "type"
-consts pname::"'a::has_pname \<Rightarrow> pname"
+class has_pname =
+  fixes pname :: "'a \<Rightarrow> pname"
 
-instance pname::has_pname ..
+instantiation pname :: has_pname
+begin
 
-defs (overloaded)
-pname_pname_def: "pname (p::pname) \<equiv> p"
+definition
+  pname_pname_def: "pname (p::pname) \<equiv> p"
 
-axclass has_tname < "type"
-consts tname::"'a::has_tname \<Rightarrow> tname"
+instance ..
+
+end
 
-instance tname::has_tname ..
+class has_tname =
+  fixes tname :: "'a \<Rightarrow> tname"
 
-defs (overloaded)
-tname_tname_def: "tname (t::tname) \<equiv> t"
+instantiation tname :: has_tname
+begin
 
-axclass has_qtname < type
-consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
+definition
+  tname_tname_def: "tname (t::tname) \<equiv> t"
+
+instance ..
 
-instance qtname_ext_type :: (type) has_qtname ..
+end
 
-defs (overloaded)
-qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
+definition
+  qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
 
 translations
   "mname"  <= "Name.mname"
diff -r 8fd9d555d04d -r fbdc860d87a3 src/HOL/Bali/Term.thy
--- a/src/HOL/Bali/Term.thy	Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/Bali/Term.thy	Tue Feb 23 10:11:12 2010 +0100
@@ -295,8 +295,8 @@
 following.
 *}
 
-axclass inj_term < "type"
-consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 1000)
+class inj_term =
+  fixes inj_term:: "'a \<Rightarrow> term" ("\<langle>_\<rangle>" 1000)
 
 text {* How this overloaded injections work can be seen in the theory 
 @{text DefiniteAssignment}. Other big inductive relations on
@@ -308,10 +308,15 @@
 as bridge between the different conventions.  
 *}
 
-instance stmt::inj_term ..
+instantiation stmt :: inj_term
+begin
 
-defs (overloaded)
-stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
+definition
+  stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
+
+instance ..
+
+end
 
 lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
 by (simp add: stmt_inj_term_def)
@@ -319,10 +324,15 @@
 lemma  stmt_inj_term [iff]: "\<langle>x::stmt\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
   by (simp add: stmt_inj_term_simp)
 
-instance expr::inj_term ..
+instantiation expr :: inj_term
+begin
 
-defs (overloaded)
-expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
+definition
+  expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
+
+instance ..
+
+end
 
 lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
 by (simp add: expr_inj_term_def)
@@ -330,10 +340,15 @@
 lemma expr_inj_term [iff]: "\<langle>x::expr\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
   by (simp add: expr_inj_term_simp)
 
-instance var::inj_term ..
+instantiation var :: inj_term
+begin
 
-defs (overloaded)
-var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
+definition
+  var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
+
+instance ..
+
+end
 
 lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
 by (simp add: var_inj_term_def)
@@ -341,10 +356,32 @@
 lemma var_inj_term [iff]: "\<langle>x::var\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
   by (simp add: var_inj_term_simp)
 
-instance "list":: (type) inj_term ..
+class expr_of =
+  fixes expr_of :: "'a \<Rightarrow> expr"
+
+instantiation expr :: expr_of
+begin
+
+definition
+  "expr_of = (\<lambda>(e::expr). e)"
+
+instance ..
+
+end 
 
-defs (overloaded)
-expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
+instantiation list :: (expr_of) inj_term
+begin
+
+definition
+  "\<langle>es::'a list\<rangle> \<equiv> In3 (map expr_of es)"
+
+instance ..
+
+end
+
+lemma expr_list_inj_term_def:
+  "\<langle>es::expr list\<rangle> \<equiv> In3 es"
+  by (simp add: inj_term_list_def expr_of_expr_def)
 
 lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
 by (simp add: expr_list_inj_term_def)
diff -r 8fd9d555d04d -r fbdc860d87a3 src/HOL/ex/PER.thy
--- a/src/HOL/ex/PER.thy	Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/ex/PER.thy	Tue Feb 23 10:11:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ex/PER.thy
-    ID:         $Id$
     Author:     Oscar Slotosch and Markus Wenzel, TU Muenchen
 *)
 
@@ -30,12 +29,10 @@
   but not necessarily reflexive.
 *}
 
-consts
-  eqv :: "'a => 'a => bool"    (infixl "\<sim>" 50)
-
-axclass partial_equiv < type
-  partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
-  partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
+class partial_equiv =
+  fixes eqv :: "'a => 'a => bool"    (infixl "\<sim>" 50)
+  assumes partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
+  assumes partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
 
 text {*
   \medskip The domain of a partial equivalence relation is the set of
@@ -70,7 +67,10 @@
   structural one corresponding to the congruence property.
 *}
 
-defs (overloaded)
+instantiation "fun" :: (partial_equiv, partial_equiv) partial_equiv
+begin
+
+definition
   eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> g y"
 
 lemma partial_equiv_funI [intro?]:
@@ -86,8 +86,7 @@
   spaces (in \emph{both} argument positions).
 *}
 
-instance "fun" :: (partial_equiv, partial_equiv) partial_equiv
-proof
+instance proof
   fix f g h :: "'a::partial_equiv => 'b::partial_equiv"
   assume fg: "f \<sim> g"
   show "g \<sim> f"
@@ -110,6 +109,8 @@
   qed
 qed
 
+end
+
 
 subsection {* Total equivalence *}
 
@@ -120,8 +121,8 @@
   symmetric.
 *}
 
-axclass equiv < partial_equiv
-  eqv_refl [intro]: "x \<sim> x"
+class equiv =
+  assumes eqv_refl [intro]: "x \<sim> x"
 
 text {*
   On total equivalences all elements are reflexive, and congruence
@@ -150,7 +151,7 @@
   \emph{equivalence classes} over elements of the base type @{typ 'a}.
 *}
 
-typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}"
+typedef 'a quot = "{{x. a \<sim> x}| a::'a::partial_equiv. True}"
   by blast
 
 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
diff -r 8fd9d555d04d -r fbdc860d87a3 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Tue Feb 23 10:11:12 2010 +0100
@@ -1417,29 +1417,20 @@
 
 (*****************************************************************************)
 
-subsubsection {* Axiomatic type classes and overloading *}
+subsubsection {* Type classes and overloading *}
 
 text {* A type class without axioms: *}
 
-axclass classA
+class classA
 
 lemma "P (x::'a::classA)"
   refute
 oops
 
-text {* The axiom of this type class does not contain any type variables: *}
-
-axclass classB
-  classB_ax: "P | ~ P"
-
-lemma "P (x::'a::classB)"
-  refute
-oops
-
 text {* An axiom with a type variable (denoting types which have at least two elements): *}
 
-axclass classC < type
-  classC_ax: "\<exists>x y. x \<noteq> y"
+class classC =
+  assumes classC_ax: "\<exists>x y. x \<noteq> y"
 
 lemma "P (x::'a::classC)"
   refute
@@ -1451,11 +1442,9 @@
 
 text {* A type class for which a constant is defined: *}
 
-consts
-  classD_const :: "'a \<Rightarrow> 'a"
-
-axclass classD < type
-  classD_ax: "classD_const (classD_const x) = classD_const x"
+class classD =
+  fixes classD_const :: "'a \<Rightarrow> 'a"
+  assumes classD_ax: "classD_const (classD_const x) = classD_const x"
 
 lemma "P (x::'a::classD)"
   refute
@@ -1463,16 +1452,12 @@
 
 text {* A type class with multiple superclasses: *}
 
-axclass classE < classC, classD
+class classE = classC + classD
 
 lemma "P (x::'a::classE)"
   refute
 oops
 
-lemma "P (x::'a::{classB, classE})"
-  refute
-oops
-
 text {* OFCLASS: *}
 
 lemma "OFCLASS('a::type, type_class)"
@@ -1485,12 +1470,6 @@
   apply intro_classes
 done
 
-lemma "OFCLASS('a, classB_class)"
-  refute  -- {* no countermodel exists *}
-  apply intro_classes
-  apply simp
-done
-
 lemma "OFCLASS('a::type, classC_class)"
   refute
 oops
diff -r 8fd9d555d04d -r fbdc860d87a3 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Mon Feb 22 17:02:39 2010 +0100
+++ b/src/Pure/Isar/class_target.ML	Tue Feb 23 10:11:12 2010 +0100
@@ -56,11 +56,6 @@
   (*tactics*)
   val intro_classes_tac: thm list -> tactic
   val default_intro_tac: Proof.context -> thm list -> tactic
-
-  (*old axclass layer*)
-  val axclass_cmd: binding * xstring list
-    -> (Attrib.binding * string list) list
-    -> theory -> class * theory
 end;
 
 structure Class_Target : CLASS_TARGET =
@@ -629,24 +624,5 @@
   Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
     "apply some intro/elim rule"));
 
-
-(** old axclass command **)
-
-fun axclass_cmd (class, raw_superclasses) raw_specs thy =
-  let
-    val _ = Output.legacy_feature "command \"axclass\" deprecated; use \"class\" instead.";
-    val ctxt = ProofContext.init thy;
-    val superclasses = map (Sign.read_class thy) raw_superclasses;
-    val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst)
-      raw_specs;
-    val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd)
-          raw_specs)
-      |> snd
-      |> (map o map) fst;
-  in
-    AxClass.define_class (class, superclasses) []
-      (name_atts ~~ axiomss) thy
-  end;
-
 end;
 
diff -r 8fd9d555d04d -r fbdc860d87a3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Feb 22 17:02:39 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Feb 23 10:11:12 2010 +0100
@@ -99,13 +99,6 @@
   OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
     (P.sort >> (Toplevel.theory o Sign.add_defsort));
 
-val _ =
-  OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
-    (P.binding -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
-        P.!!! (P.list1 P.xname)) []
-        -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
-      >> (fn (x, y) => Toplevel.theory (snd o Class.axclass_cmd x y)));
-
 
 (* types *)