diff -r 5b466efedd2c -r 63beb38e9258 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Feb 21 00:09:55 2014 +0100
+++ b/src/HOL/List.thy	Fri Feb 21 00:09:56 2014 +0100
@@ -1645,10 +1645,10 @@
 lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
 apply (induct xs, simp, simp)
 apply safe
-apply (metis nat.cases(1) nth.simps zero_less_Suc)
+apply (metis nat.case(1) nth.simps zero_less_Suc)
 apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
 apply (case_tac i, simp)
-apply (metis diff_Suc_Suc nat.cases(2) nth.simps zero_less_diff)
+apply (metis diff_Suc_Suc nat.case(2) nth.simps zero_less_diff)
 done
 
 lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"