outermost universal quantifiers are stripped

--- a/src/HOL/ex/Refute_Examples.thy	Mon Nov 27 17:13:10 2006 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Mon Nov 27 17:35:50 2006 +0100
@@ -163,8 +163,7 @@
 oops
 
 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 *}
+  refute
 oops
 
 text {* "Every reflexive and symmetric relation is transitive." *}