diff -r ab3dfcef6489 -r 98e3e9f00192 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Fri Jan 19 21:20:10 2007 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Fri Jan 19 22:04:22 2007 +0100
@@ -980,6 +980,10 @@
   refute
 oops
 
+lemma "x \<in> Finites"
+  refute  -- {* no finite countermodel exists *}
+oops
+
 lemma "finite x"
   refute  -- {* no finite countermodel exists *}
 oops