--- a/PrioG.thy	Thu Dec 06 15:12:49 2012 +0000
+++ b/PrioG.thy	Thu Dec 06 15:49:20 2012 +0000
@@ -1033,7 +1033,8 @@
           show ?thesis by (unfold h, simp)
         next
           assume "\<exists> a. ?D = {a}"
-          thus ?thesis by auto
+          thus ?thesis
+            by (metis finite.simps)
         qed
       qed
       ultimately show ?thesis by simp