prefer ex1I over ex_ex1I in single-step reasoning;

--- a/src/HOL/HOL.thy	Sat Jan 14 22:25:34 2006 +0100
+++ b/src/HOL/HOL.thy	Sun Jan 15 19:58:51 2006 +0100
@@ -918,6 +918,9 @@
 setup Classical.setup
 setup clasetup
 
+declare ex_ex1I [rule del, intro! 2]
+  and ex1I [intro]
+
 lemmas [intro?] = ext
   and [elim?] = ex1_implies_ex
 

--- a/src/HOL/Real/HahnBanach/Subspace.thy	Sat Jan 14 22:25:34 2006 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Sun Jan 15 19:58:51 2006 +0100
@@ -435,7 +435,7 @@
 proof -
   from x y x' have "x \<in> H + lin x'" by auto
   have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p")
-  proof
+  proof (rule ex_ex1I)
     from x y show "\<exists>p. ?P p" by blast
     fix p q assume p: "?P p" and q: "?P q"
     show "p = q"
@@ -450,7 +450,6 @@
         from xq show "fst q \<in> H" ..
         from xp and xq show "fst p + snd p \<cdot> x' = fst q + snd q \<cdot> x'"
           by simp
-        apply_end assumption+
       qed
       thus ?thesis by (cases p, cases q) simp
     qed