subclass now also works for subclasses with empty specificaton

--- a/src/Pure/Isar/class.ML	Fri Jul 25 12:03:36 2008 +0200
+++ b/src/Pure/Isar/class.ML	Fri Jul 25 12:03:37 2008 +0200
@@ -22,7 +22,7 @@
 
   val intro_classes_tac: thm list -> tactic
   val default_intro_tac: Proof.context -> thm list -> tactic
-  val prove_subclass: class * class -> thm -> theory -> theory
+  val prove_subclass: class * class -> thm option -> theory -> theory
 
   val class_prefix: string -> string
   val is_class: theory -> class -> bool
@@ -338,7 +338,7 @@
   in
     thy
     |> Sign.sticky_prefix (class_prefix class ^ "_" ^ AxClass.axiomsN)
-    |> PureThy.note Thm.internalK (AxClass.introN, this_intro)
+    |> PureThy.store_thm (AxClass.introN, this_intro)
     |> snd
     |> Sign.restore_naming thy
     |> pair (morphism, axiom, assm_intro, of_class)
@@ -362,15 +362,19 @@
     |> fold2 add_constraint (map snd consts) constraints
   end;
 
-fun prove_subclass (sub, sup) thm thy =
+fun prove_subclass (sub, sup) some_thm thy =
   let
     val of_class = (#of_class o the_class_data thy) sup;
-    val intro = Drule.standard' (of_class OF [Drule.standard' thm]);
-    val classrel = intro OF (the_list o #axiom o the_class_data thy) sub;
+    val intro = case some_thm
+     of SOME thm => Drule.standard' (of_class OF [Drule.standard' thm])
+      | NONE => Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
+          ([], [sub])], []) of_class;
+    val classrel = (intro OF (the_list o #axiom o the_class_data thy) sub)
+      |> Thm.close_derivation;
   in
     thy
     |> AxClass.add_classrel classrel
-    |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac [thm]))
+    |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac (the_list some_thm)))
          I (sub, Locale.Locale sup)
     |> ClassData.map (Graph.add_edge (sub, sup))
   end;
@@ -557,7 +561,7 @@
       prep_spec thy raw_supclasses raw_elems;
   in
     thy
-    |> Locale.add_locale_i (SOME "") bname mergeexpr elems
+    |> Locale.add_locale_i "" bname mergeexpr elems
     |> snd
     |> ProofContext.theory_of
     |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
@@ -602,7 +606,7 @@
     ||>> get_axiom
     |-> (fn (def, def') => class_interpretation class [def] [Thm.prop_of def]
       #> register_operation class (c', (dict', SOME (Thm.symmetric def')))
-      #> PureThy.note Thm.internalK (c ^ "_raw", def')
+      #> PureThy.store_thm (c ^ "_raw", def')
       #> snd)
     |> Sign.restore_naming thy
     |> Sign.add_const_constraint (c', SOME ty')

--- a/src/Pure/Isar/subclass.ML	Fri Jul 25 12:03:36 2008 +0200
+++ b/src/Pure/Isar/subclass.ML	Fri Jul 25 12:03:37 2008 +0200
@@ -17,6 +17,10 @@
 
 local
 
+fun the_option [x] = SOME x
+  | the_option [] = NONE
+  | the_option _ = raise Empty;
+
 fun gen_subclass prep_class do_proof raw_sup lthy =
   let
     val thy = ProofContext.theory_of lthy;
@@ -24,6 +28,10 @@
     val sub = case TheoryTarget.peek lthy
      of {is_class = false, ...} => error "No class context"
       | {target, ...} => target;
+    val _ = if Sign.subsort thy ([sup], [sub])
+      then error ("Class " ^ Syntax.string_of_sort lthy [sup]
+        ^ " is subclass of class " ^ Syntax.string_of_sort lthy [sub])
+      else ();
     val sub_params = map fst (Class.these_params thy [sub]);
     val sup_params = map fst (Class.these_params thy [sup]);
     val err_params = subtract (op =) sub_params sup_params;
@@ -33,21 +41,25 @@
     val sublocale_prop =
       Locale.global_asms_of thy sup
       |> maps snd
-      |> the_single
-      |> ObjectLogic.ensure_propT thy;
-    fun after_qed thm =
-      LocalTheory.theory (Class.prove_subclass (sub, sup) thm)
+      |> the_option
+      |> Option.map (ObjectLogic.ensure_propT thy);
+    fun after_qed some_thm =
+      LocalTheory.theory (Class.prove_subclass (sub, sup) some_thm)
       #> (TheoryTarget.init (SOME sub) o ProofContext.theory_of);
   in
     do_proof after_qed sublocale_prop lthy
   end;
 
-fun user_proof after_qed prop =
-  Proof.theorem_i NONE (after_qed o the_single o the_single) [[(prop, [])]];
+fun user_proof after_qed NONE =
+      Proof.theorem_i NONE (K (after_qed NONE)) [[]]
+  | user_proof after_qed (SOME prop) =
+      Proof.theorem_i NONE (after_qed o the_option o the_single) [[(prop, [])]];
 
-fun tactic_proof tac after_qed prop lthy =
-  after_qed (Goal.prove (LocalTheory.target_of lthy) [] [] prop
-    (K tac)) lthy;
+fun tactic_proof tac after_qed NONE lthy =
+      after_qed NONE lthy
+  | tactic_proof tac after_qed (SOME prop) lthy =
+      after_qed (SOME (Goal.prove (LocalTheory.target_of lthy) [] [] prop
+        (K tac))) lthy;
 
 in