1.1 --- a/src/HOL/Library/RBT_Impl.thy	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -1167,7 +1167,7 @@
     1.4            apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
     1.5        else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
     1.6            apfst (Branch B t1 k v) (rbtreeify_f n' kvs'))"
     1.7 -by(subst rbtreeify_f.simps)(simp only: Let_def divmod_nat_div_mod prod.simps)
     1.8 +by (subst rbtreeify_f.simps) (simp only: Let_def divmod_nat_div_mod prod.case)
     1.9  
    1.10  lemma rbtreeify_g_code [code]:
    1.11    "rbtreeify_g n kvs =
    1.12 @@ -1178,7 +1178,7 @@
    1.13            apfst (Branch B t1 k v) (rbtreeify_g n' kvs')
    1.14        else case rbtreeify_f n' kvs of (t1, (k, v) # kvs') \<Rightarrow>
    1.15            apfst (Branch B t1 k v) (rbtreeify_g n' kvs'))"
    1.16 -by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_div_mod prod.simps)
    1.17 +by(subst rbtreeify_g.simps)(simp only: Let_def divmod_nat_div_mod prod.case)
    1.18  
    1.19  lemma Suc_double_half: "Suc (2 * n) div 2 = n"
    1.20  by simp
    1.21 @@ -1250,8 +1250,8 @@
    1.22        with "1.prems" False obtain t1 k' v' kvs''
    1.23          where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
    1.24           by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm)
    1.25 -      note this also note prod.simps(2) also note list.simps(5) 
    1.26 -      also note prod.simps(2) also note snd_apfst
    1.27 +      note this also note prod.case also note list.simps(5) 
    1.28 +      also note prod.case also note snd_apfst
    1.29        also have "0 < n div 2" "n div 2 \<le> Suc (length kvs'')" 
    1.30          using len "1.prems" False unfolding kvs'' by simp_all
    1.31        with True kvs''[symmetric] refl refl
    1.32 @@ -1276,8 +1276,8 @@
    1.33        with "1.prems" `\<not> n \<le> 1` obtain t1 k' v' kvs''
    1.34          where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
    1.35          by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm)
    1.36 -      note this also note prod.simps(2) also note list.simps(5) 
    1.37 -      also note prod.simps(2) also note snd_apfst
    1.38 +      note this also note prod.case also note list.simps(5)
    1.39 +      also note prod.case also note snd_apfst
    1.40        also have "n div 2 \<le> length kvs''" 
    1.41          using len "1.prems" False unfolding kvs'' by simp arith
    1.42        with False kvs''[symmetric] refl refl
    1.43 @@ -1315,8 +1315,8 @@
    1.44        with "2.prems" obtain t1 k' v' kvs''
    1.45          where kvs'': "rbtreeify_g (n div 2) kvs = (t1, (k', v') # kvs'')"
    1.46          by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm)
    1.47 -      note this also note prod.simps(2) also note list.simps(5) 
    1.48 -      also note prod.simps(2) also note snd_apfst
    1.49 +      note this also note prod.case also note list.simps(5) 
    1.50 +      also note prod.case also note snd_apfst
    1.51        also have "n div 2 \<le> Suc (length kvs'')" 
    1.52          using len "2.prems" unfolding kvs'' by simp
    1.53        with True kvs''[symmetric] refl refl `0 < n div 2`
    1.54 @@ -1341,8 +1341,8 @@
    1.55        with "2.prems" `1 < n` False obtain t1 k' v' kvs'' 
    1.56          where kvs'': "rbtreeify_f (n div 2) kvs = (t1, (k', v') # kvs'')"
    1.57          by(cases ?rest1)(auto simp add: snd_def split: prod.split_asm, arith)
    1.58 -      note this also note prod.simps(2) also note list.simps(5) 
    1.59 -      also note prod.simps(2) also note snd_apfst
    1.60 +      note this also note prod.case also note list.simps(5) 
    1.61 +      also note prod.case also note snd_apfst
    1.62        also have "n div 2 \<le> Suc (length kvs'')" 
    1.63          using len "2.prems" False unfolding kvs'' by simp arith
    1.64        with False kvs''[symmetric] refl refl `0 < n div 2`