smaller example to prevent timeout

--- a/src/HOL/ex/Refute_Examples.thy	Thu Jan 26 17:58:01 2006 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Thu Jan 26 20:17:54 2006 +0100
@@ -156,13 +156,13 @@
   apply fast
 done
 
-text {* "A type has at most 5 elements." *}
+text {* "A type has at most 4 elements." *}
 
-lemma "a=b | a=c | a=d | a=e | a=f | b=c | b=d | b=e | b=f | c=d | c=e | c=f | d=e | d=f | e=f"
+lemma "a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e"
   refute
 oops
 
-lemma "\<forall>a b c d e f. a=b | a=c | a=d | a=e | a=f | b=c | b=d | b=e | b=f | c=d | c=e | c=f | d=e | d=f | e=f"
+lemma "\<forall>a b c d e. a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e"
   refute  -- {* quantification causes an expansion of the formula; the
                 previous version with free variables is refuted much faster *}
 oops