diff -r 27de2c976d90 -r eb2caacf3ba4 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Library/RBT_Impl.thy	Wed Feb 12 08:35:56 2014 +0100
@@ -1167,7 +1167,7 @@
           apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
       else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
           apfst (Branch B t1 k v) (rbtreeify_f n' kvs'))"
-by(subst rbtreeify_f.simps)(simp only: Let_def divmod_nat_div_mod prod.simps)
+by (subst rbtreeify_f.simps) (simp only: Let_def divmod_nat_div_mod prod.case)
 
 lemma rbtreeify_g_code [code]:
   "rbtreeify_g n kvs =
@@ -1178,7 +1178,7 @@
           apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
       else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
           apfst (Branch B t1 k v) (rbtreeify_g n' kvs'))"
-by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_div_mod prod.simps)
+by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_div_mod prod.case)
 
 lemma Suc_double_half: "Suc (2 * n) div 2 = n"
 by simp
@@ -1250,8 +1250,8 @@
       with "1.prems" False obtain t1 k' v' kvs''
         where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
          by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm)
-      note this also note prod.simps(2) also note list.simps(5) 
-      also note prod.simps(2) also note snd_apfst
+      note this also note prod.case also note list.simps(5) 
+      also note prod.case also note snd_apfst
       also have "0 < n div 2" "n div 2 \<le> Suc (length kvs'')" 
         using len "1.prems" False unfolding kvs'' by simp_all
       with True kvs''[symmetric] refl refl
@@ -1276,8 +1276,8 @@
       with "1.prems" `\<not> n \<le> 1` obtain t1 k' v' kvs''
         where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
         by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm)
-      note this also note prod.simps(2) also note list.simps(5) 
-      also note prod.simps(2) also note snd_apfst
+      note this also note prod.case also note list.simps(5)
+      also note prod.case also note snd_apfst
       also have "n div 2 \<le> length kvs''" 
         using len "1.prems" False unfolding kvs'' by simp arith
       with False kvs''[symmetric] refl refl
@@ -1315,8 +1315,8 @@
       with "2.prems" obtain t1 k' v' kvs''
         where kvs'': "rbtreeify_g (n div 2) kvs = (t1, (k', v') # kvs'')"
         by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm)
-      note this also note prod.simps(2) also note list.simps(5) 
-      also note prod.simps(2) also note snd_apfst
+      note this also note prod.case also note list.simps(5) 
+      also note prod.case also note snd_apfst
       also have "n div 2 \<le> Suc (length kvs'')" 
         using len "2.prems" unfolding kvs'' by simp
       with True kvs''[symmetric] refl refl `0 < n div 2`
@@ -1341,8 +1341,8 @@
       with "2.prems" `1 < n` False obtain t1 k' v' kvs'' 
         where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
         by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm, arith)
-      note this also note prod.simps(2) also note list.simps(5) 
-      also note prod.simps(2) also note snd_apfst
+      note this also note prod.case also note list.simps(5) 
+      also note prod.case also note snd_apfst
       also have "n div 2 \<le> Suc (length kvs'')" 
         using len "2.prems" False unfolding kvs'' by simp arith
       with False kvs''[symmetric] refl refl `0 < n div 2`