--- a/src/HOL/Word/Word.thy Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Word/Word.thy Tue Oct 13 09:21:15 2015 +0200
@@ -3836,7 +3836,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: Product_Type.split_split)
+ by (simp add: bin_rsplit_aux_simp_alt Let_def split: prod.split)
lemma test_bit_rsplit:
"sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a :: len word) \<Longrightarrow>