removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly

--- a/src/HOL/List.thy	Wed Feb 08 00:05:22 2012 +0100
+++ b/src/HOL/List.thy	Wed Feb 08 00:55:06 2012 +0100
@@ -934,7 +934,7 @@
 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
 by (cases xs) auto
 
-lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
+lemma rev_is_rev_conv [iff, no_atp]: "(rev xs = rev ys) = (xs = ys)"
 apply (induct xs arbitrary: ys, force)
 apply (case_tac ys, simp, force)
 done