# HG changeset patch
# User paulson
# Date 1108373098 -3600
# Node ID 9712d41db5b8a6b2d5083ca4ecdab767d80b8321
# Parent  08c8dad8e3990a9c814c578017e9eca0c24b1a33
simplified a proof

diff -r 08c8dad8e399 -r 9712d41db5b8 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Feb 13 17:15:14 2005 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Feb 14 10:24:58 2005 +0100
@@ -548,8 +548,7 @@
   case (Suc m)
   have nSuc: "n = Suc m" . 
   have mlessn: "m<n" by (simp add: nSuc)
-  have "a \<in> h ` {i. i < n}" using aA by blast
-  then obtain k where hkeq: "h k = a" and klessn: "k<n" by blast
+  from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
   let ?hm = "swap k m h"
   have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn 
     by (simp add: inj_on_swap_iff inj_on)