# HG changeset patch
# User haftmann
# Date 1244992819 -7200
# Node ID 8623244a50d568d3780657bfee64b6123b96eb97
# Parent  cb3bb7f79792a6a7e59d9ea5bb924c99d73c181e
axclass command now legacy

diff -r cb3bb7f79792 -r 8623244a50d5 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Sun Jun 14 17:20:19 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Sun Jun 14 17:20:19 2009 +0200
@@ -10,8 +10,6 @@
   val register: class -> class list -> ((string * typ) * (string * typ)) list
     -> sort -> morphism -> thm option -> thm option -> thm
     -> theory -> theory
-  val register_subclass: class * class -> morphism option -> Element.witness option
-    -> morphism -> theory -> theory
 
   val is_class: theory -> class -> bool
   val base_sort: theory -> class -> sort
@@ -46,8 +44,16 @@
   val instantiation_param: local_theory -> binding -> string option
   val confirm_declaration: binding -> local_theory -> local_theory
   val pretty_instantiation: local_theory -> Pretty.T
+  val instance_arity_cmd: xstring * xstring list * xstring -> theory -> Proof.state
   val type_name: string -> string
 
+  (*subclasses*)
+  val register_subclass: class * class -> morphism option -> Element.witness option
+    -> morphism -> theory -> theory
+  val classrel: class * class -> theory -> Proof.state
+  val classrel_cmd: xstring * xstring -> theory -> Proof.state
+
+  (*tactics*)
   val intro_classes_tac: thm list -> tactic
   val default_intro_tac: Proof.context -> thm list -> tactic
 
@@ -55,58 +61,11 @@
   val axclass_cmd: binding * xstring list
     -> (Attrib.binding * string list) list
     -> theory -> class * theory
-  val classrel_cmd: xstring * xstring -> theory -> Proof.state
-  val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state
-  val instance_arity_cmd: xstring * xstring list * xstring -> theory -> Proof.state
 end;
 
 structure Class_Target : CLASS_TARGET =
 struct
 
-(** primitive axclass and instance commands **)
-
-fun axclass_cmd (class, raw_superclasses) raw_specs thy =
-  let
-    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;
-
-local
-
-fun gen_instance mk_prop add_thm after_qed insts thy =
-  let
-    fun after_qed' results =
-      ProofContext.theory ((fold o fold) add_thm results #> after_qed);
-  in
-    thy
-    |> ProofContext.init
-    |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])])
-        o mk_prop thy) insts)
-  end;
-
-in
-
-val instance_arity =
-  gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
-val instance_arity_cmd =
-  gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity I;
-val classrel =
-  gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) AxClass.add_classrel I;
-val classrel_cmd =
-  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I;
-
-end; (*local*)
-
-
 (** class data **)
 
 datatype class_data = ClassData of {
@@ -276,7 +235,7 @@
       [Option.map (Drule.standard' o Element.conclude_witness) some_wit,
         (fst o rules thy) sub];
     val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
-    val classrel = Goal.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
+    val classrel = SkipProof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
       (K tac);
     val diff_sort = Sign.complete_sort thy [sup]
       |> subtract (op =) (Sign.complete_sort thy [sub])
@@ -403,6 +362,30 @@
   end;
 
 
+(* simple subclasses *)
+
+local
+
+fun gen_classrel mk_prop classrel thy =
+  let
+    fun after_qed results =
+      ProofContext.theory ((fold o fold) AxClass.add_classrel results);
+  in
+    thy
+    |> ProofContext.init
+    |> Proof.theorem_i NONE after_qed [[(mk_prop thy classrel, [])]]
+  end;
+
+in
+
+val classrel =
+  gen_classrel (Logic.mk_classrel oo AxClass.cert_classrel);
+val classrel_cmd =
+  gen_classrel (Logic.mk_classrel oo AxClass.read_classrel);
+
+end; (*local*)
+
+
 (** instantiation target **)
 
 (* bookkeeping *)
@@ -593,6 +576,20 @@
   end;
 
 
+(* simplified instantiation interface with no class parameter *)
+
+fun instance_arity_cmd arities thy =
+  let
+    fun after_qed results = ProofContext.theory
+      ((fold o fold) AxClass.add_arity results);
+  in
+    thy
+    |> ProofContext.init
+    |> Proof.theorem_i NONE after_qed ((map (fn t => [(t, [])])
+        o Logic.mk_arities o Sign.read_arity thy) arities)
+  end;
+
+
 (** tactics and methods **)
 
 fun intro_classes_tac facts st =
@@ -620,5 +617,24 @@
   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;