explicit is better than implicit;

--- a/src/HOL/List.thy	Wed Feb 02 22:48:24 2011 +0100
+++ b/src/HOL/List.thy	Thu Feb 03 18:57:42 2011 +0100
@@ -456,7 +456,9 @@
   "xs \<noteq> x # xs"
 by (induct xs) auto
 
-lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric]
+lemma not_Cons_self2 [simp]:
+  "x # xs \<noteq> xs"
+by (rule not_Cons_self [symmetric])
 
 lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)"
 by (induct xs) auto