diff -r 89b9f7c18631 -r 9d2c375e242b src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Sat Mar 15 22:07:28 2008 +0100
+++ b/src/HOL/Word/WordShift.thy	Sat Mar 15 22:07:29 2008 +0100
@@ -1093,7 +1093,7 @@
 lemma word_rsplit_empty_iff_size:
   "(word_rsplit w = []) = (size w = 0)" 
   unfolding word_rsplit_def bin_rsplit_def word_size
-  by (simp add: bin_rsplit_aux_simp_alt Let_def split: split_split)
+  by (simp add: bin_rsplit_aux_simp_alt Let_def split: Product_Type.split_split)
 
 lemma test_bit_rsplit:
   "sw = word_rsplit w ==> m < size (hd sw :: 'a :: len word) ==>