diff -r 6407d832da03 -r a4ffa756d8eb src/HOL/MetisExamples/Abstraction.thy
--- a/src/HOL/MetisExamples/Abstraction.thy	Fri Jun 29 16:05:00 2007 +0200
+++ b/src/HOL/MetisExamples/Abstraction.thy	Fri Jun 29 18:21:25 2007 +0200
@@ -75,19 +75,13 @@
 assume 1: "\<And>f x. llabs_subgoal_1 f x = Collect (COMBB (op = x) f)"
 assume 2: "a \<notin> A \<or> a \<noteq> f b"
 have 3: "a \<in> A"
-  by (metis SigmaD1 0)
-have 4: "b \<in> llabs_subgoal_1 f a"
-  by (metis SigmaD2 0)
-have 5: "\<And>X1 X2. X2 -` {X1} = llabs_subgoal_1 X2 X1"
-  by (metis 1 vimage_Collect_eq singleton_conv2)
-have 6: "\<And>X1 X2 X3. X1 X2 = X3 \<or> X2 \<notin> llabs_subgoal_1 X1 X3"
-  by (metis vimage_singleton_eq 5)
-have 7: "f b \<noteq> a"
-  by (metis 2 3)
-have 8: "f b = a"
-  by (metis 6 4)
+  by (metis member2_def SigmaD1 0)
+have 4: "f b \<noteq> a"
+  by (metis 3 2)
+have 5: "f b = a"
+  by (metis Domain_Id Compl_UNIV_eq singleton_conv2 vimage_Collect_eq 1 vimage_singleton_eq SigmaD2 member2_def 0)
 show "False"
-  by (metis 8 7)
+  by (metis 5 4)
 qed finish_clausify