tuned
authorhaftmann
Thu Nov 06 09:09:49 2008 +0100 (2008-11-06)
changeset 28716ee6f9e50f9c8
parent 28715 238f9966c80e
child 28717 848ffc6b0b8a
tuned
src/Pure/Isar/subclass.ML
     1.1 --- a/src/Pure/Isar/subclass.ML	Thu Nov 06 09:09:48 2008 +0100
     1.2 +++ b/src/Pure/Isar/subclass.ML	Thu Nov 06 09:09:49 2008 +0100
     1.3 @@ -17,10 +17,6 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun the_option [x] = SOME x
     1.8 -  | the_option [] = NONE
     1.9 -  | the_option _ = raise Empty;
    1.10 -
    1.11  fun gen_subclass prep_class do_proof raw_sup lthy =
    1.12    let
    1.13      val thy = ProofContext.theory_of lthy;
    1.14 @@ -41,7 +37,7 @@
    1.15      val sublocale_prop =
    1.16        Locale.global_asms_of thy sup
    1.17        |> maps snd
    1.18 -      |> the_option
    1.19 +      |> try the_single
    1.20        |> Option.map (ObjectLogic.ensure_propT thy);
    1.21      fun after_qed some_thm =
    1.22        LocalTheory.theory (Class.prove_subclass (sub, sup) some_thm)
    1.23 @@ -53,7 +49,7 @@
    1.24  fun user_proof after_qed NONE =
    1.25        Proof.theorem_i NONE (K (after_qed NONE)) [[]]
    1.26    | user_proof after_qed (SOME prop) =
    1.27 -      Proof.theorem_i NONE (after_qed o the_option o the_single) [[(prop, [])]];
    1.28 +      Proof.theorem_i NONE (after_qed o try the_single o the_single) [[(prop, [])]];
    1.29  
    1.30  fun tactic_proof tac after_qed NONE lthy =
    1.31        after_qed NONE lthy