src/HOL/Word/Word.thy

--- a/src/HOL/Word/Word.thy	Wed Feb 08 00:55:06 2012 +0100
+++ b/src/HOL/Word/Word.thy	Wed Feb 08 01:49:33 2012 +0100
@@ -3942,7 +3942,7 @@
     rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)" 
   apply (unfold map2_def)
   apply (cases xs)
-   apply (cases ys, auto simp add : rotate1_def)+
+   apply (cases ys, auto)+
   done
 
 lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]