1.1 --- a/src/Pure/Isar/class.ML	Fri Jul 25 12:03:36 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Jul 25 12:03:37 2008 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4  
     1.5    val intro_classes_tac: thm list -> tactic
     1.6    val default_intro_tac: Proof.context -> thm list -> tactic
     1.7 -  val prove_subclass: class * class -> thm -> theory -> theory
     1.8 +  val prove_subclass: class * class -> thm option -> theory -> theory
     1.9  
    1.10    val class_prefix: string -> string
    1.11    val is_class: theory -> class -> bool
    1.12 @@ -338,7 +338,7 @@
    1.13    in
    1.14      thy
    1.15      |> Sign.sticky_prefix (class_prefix class ^ "_" ^ AxClass.axiomsN)
    1.16 -    |> PureThy.note Thm.internalK (AxClass.introN, this_intro)
    1.17 +    |> PureThy.store_thm (AxClass.introN, this_intro)
    1.18      |> snd
    1.19      |> Sign.restore_naming thy
    1.20      |> pair (morphism, axiom, assm_intro, of_class)
    1.21 @@ -362,15 +362,19 @@
    1.22      |> fold2 add_constraint (map snd consts) constraints
    1.23    end;
    1.24  
    1.25 -fun prove_subclass (sub, sup) thm thy =
    1.26 +fun prove_subclass (sub, sup) some_thm thy =
    1.27    let
    1.28      val of_class = (#of_class o the_class_data thy) sup;
    1.29 -    val intro = Drule.standard' (of_class OF [Drule.standard' thm]);
    1.30 -    val classrel = intro OF (the_list o #axiom o the_class_data thy) sub;
    1.31 +    val intro = case some_thm
    1.32 +     of SOME thm => Drule.standard' (of_class OF [Drule.standard' thm])
    1.33 +      | NONE => Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
    1.34 +          ([], [sub])], []) of_class;
    1.35 +    val classrel = (intro OF (the_list o #axiom o the_class_data thy) sub)
    1.36 +      |> Thm.close_derivation;
    1.37    in
    1.38      thy
    1.39      |> AxClass.add_classrel classrel
    1.40 -    |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac [thm]))
    1.41 +    |> prove_interpretation_in (ALLGOALS (ProofContext.fact_tac (the_list some_thm)))
    1.42           I (sub, Locale.Locale sup)
    1.43      |> ClassData.map (Graph.add_edge (sub, sup))
    1.44    end;
    1.45 @@ -557,7 +561,7 @@
    1.46        prep_spec thy raw_supclasses raw_elems;
    1.47    in
    1.48      thy
    1.49 -    |> Locale.add_locale_i (SOME "") bname mergeexpr elems
    1.50 +    |> Locale.add_locale_i "" bname mergeexpr elems
    1.51      |> snd
    1.52      |> ProofContext.theory_of
    1.53      |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
    1.54 @@ -602,7 +606,7 @@
    1.55      ||>> get_axiom
    1.56      |-> (fn (def, def') => class_interpretation class [def] [Thm.prop_of def]
    1.57        #> register_operation class (c', (dict', SOME (Thm.symmetric def')))
    1.58 -      #> PureThy.note Thm.internalK (c ^ "_raw", def')
    1.59 +      #> PureThy.store_thm (c ^ "_raw", def')
    1.60        #> snd)
    1.61      |> Sign.restore_naming thy
    1.62      |> Sign.add_const_constraint (c', SOME ty')

     2.1 --- a/src/Pure/Isar/subclass.ML	Fri Jul 25 12:03:36 2008 +0200
     2.2 +++ b/src/Pure/Isar/subclass.ML	Fri Jul 25 12:03:37 2008 +0200
     2.3 @@ -17,6 +17,10 @@
     2.4  
     2.5  local
     2.6  
     2.7 +fun the_option [x] = SOME x
     2.8 +  | the_option [] = NONE
     2.9 +  | the_option _ = raise Empty;
    2.10 +
    2.11  fun gen_subclass prep_class do_proof raw_sup lthy =
    2.12    let
    2.13      val thy = ProofContext.theory_of lthy;
    2.14 @@ -24,6 +28,10 @@
    2.15      val sub = case TheoryTarget.peek lthy
    2.16       of {is_class = false, ...} => error "No class context"
    2.17        | {target, ...} => target;
    2.18 +    val _ = if Sign.subsort thy ([sup], [sub])
    2.19 +      then error ("Class " ^ Syntax.string_of_sort lthy [sup]
    2.20 +        ^ " is subclass of class " ^ Syntax.string_of_sort lthy [sub])
    2.21 +      else ();
    2.22      val sub_params = map fst (Class.these_params thy [sub]);
    2.23      val sup_params = map fst (Class.these_params thy [sup]);
    2.24      val err_params = subtract (op =) sub_params sup_params;
    2.25 @@ -33,21 +41,25 @@
    2.26      val sublocale_prop =
    2.27        Locale.global_asms_of thy sup
    2.28        |> maps snd
    2.29 -      |> the_single
    2.30 -      |> ObjectLogic.ensure_propT thy;
    2.31 -    fun after_qed thm =
    2.32 -      LocalTheory.theory (Class.prove_subclass (sub, sup) thm)
    2.33 +      |> the_option
    2.34 +      |> Option.map (ObjectLogic.ensure_propT thy);
    2.35 +    fun after_qed some_thm =
    2.36 +      LocalTheory.theory (Class.prove_subclass (sub, sup) some_thm)
    2.37        #> (TheoryTarget.init (SOME sub) o ProofContext.theory_of);
    2.38    in
    2.39      do_proof after_qed sublocale_prop lthy
    2.40    end;
    2.41  
    2.42 -fun user_proof after_qed prop =
    2.43 -  Proof.theorem_i NONE (after_qed o the_single o the_single) [[(prop, [])]];
    2.44 +fun user_proof after_qed NONE =
    2.45 +      Proof.theorem_i NONE (K (after_qed NONE)) [[]]
    2.46 +  | user_proof after_qed (SOME prop) =
    2.47 +      Proof.theorem_i NONE (after_qed o the_option o the_single) [[(prop, [])]];
    2.48  
    2.49 -fun tactic_proof tac after_qed prop lthy =
    2.50 -  after_qed (Goal.prove (LocalTheory.target_of lthy) [] [] prop
    2.51 -    (K tac)) lthy;
    2.52 +fun tactic_proof tac after_qed NONE lthy =
    2.53 +      after_qed NONE lthy
    2.54 +  | tactic_proof tac after_qed (SOME prop) lthy =
    2.55 +      after_qed (SOME (Goal.prove (LocalTheory.target_of lthy) [] [] prop
    2.56 +        (K tac))) lthy;
    2.57  
    2.58  in
    2.59