# HG changeset patch
# User haftmann
# Date 1225958989 -3600
# Node ID ee6f9e50f9c8a891de56f31e3f239bb52b1c9a3a
# Parent  238f9966c80eb12d24ca9c4938fba872727fed44
tuned

diff -r 238f9966c80e -r ee6f9e50f9c8 src/Pure/Isar/subclass.ML
--- a/src/Pure/Isar/subclass.ML	Thu Nov 06 09:09:48 2008 +0100
+++ b/src/Pure/Isar/subclass.ML	Thu Nov 06 09:09:49 2008 +0100
@@ -17,10 +17,6 @@
 
 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;
@@ -41,7 +37,7 @@
     val sublocale_prop =
       Locale.global_asms_of thy sup
       |> maps snd
-      |> the_option
+      |> try the_single
       |> Option.map (ObjectLogic.ensure_propT thy);
     fun after_qed some_thm =
       LocalTheory.theory (Class.prove_subclass (sub, sup) some_thm)
@@ -53,7 +49,7 @@
 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, [])]];
+      Proof.theorem_i NONE (after_qed o try the_single o the_single) [[(prop, [])]];
 
 fun tactic_proof tac after_qed NONE lthy =
       after_qed NONE lthy