# HG changeset patch
# User wenzelm
# Date 1118311400 -7200
# Node ID 490d778206310aab1c66f1aaaf79d2ccc995edc7
# Parent  25a440fe5f65dc3416c413153aab49d6b31d9fbe
got rid of bclass, xclass;

diff -r 25a440fe5f65 -r 490d77820631 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Thu Jun 09 12:03:19 2005 +0200
+++ b/src/Pure/axclass.ML	Thu Jun 09 12:03:20 2005 +0200
@@ -9,17 +9,17 @@
 sig
   val quiet_mode: bool ref
   val print_axclasses: theory -> unit
-  val add_axclass: bclass * xclass list -> ((bstring * string) * Attrib.src list) list
+  val add_axclass: bstring * xstring list -> ((bstring * string) * Attrib.src list) list
     -> theory -> theory * {intro: thm, axioms: thm list}
-  val add_axclass_i: bclass * class list -> ((bstring * term) * theory attribute list) list
+  val add_axclass_i: bstring * class list -> ((bstring * term) * theory attribute list) list
     -> theory -> theory * {intro: thm, axioms: thm list}
   val add_classrel_thms: thm list -> theory -> theory
   val add_arity_thms: thm list -> theory -> theory
-  val add_inst_subclass: xclass * xclass -> tactic -> 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: xstring * string list * string -> tactic -> theory -> theory
   val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
-  val instance_subclass_proof: xclass * xclass -> bool -> theory -> ProofHistory.T
+  val instance_subclass_proof: xstring * xstring -> bool -> theory -> ProofHistory.T
   val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T
   val instance_arity_proof: xstring * string list * string -> bool -> theory -> ProofHistory.T
   val instance_arity_proof_i: string * sort list * sort -> bool -> theory -> ProofHistory.T
@@ -28,7 +28,7 @@
 
   (*legacy interfaces*)
   val axclass_tac: thm list -> tactic
-  val add_inst_subclass_x: xclass * xclass -> string list -> thm list
+  val add_inst_subclass_x: xstring * xstring -> string list -> thm list
     -> tactic option -> theory -> theory
   val add_inst_arity_x: xstring * string list * string -> string list
     -> thm list -> tactic option -> theory -> theory