author haftmann Thu Nov 06 09:09:49 2008 +0100 (2008-11-06) changeset 28716 ee6f9e50f9c8 parent 28715 238f9966c80e child 28717 848ffc6b0b8a
tuned
```     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
```