--- a/src/HOL/List.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/List.thy Wed Feb 12 08:37:06 2014 +0100
@@ -1648,10 +1648,10 @@
lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
apply (induct xs, simp, simp)
apply safe
-apply (metis case_nat_0 nth.simps zero_less_Suc)
+apply (metis nat.cases(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 case_nat_Suc nth.simps zero_less_diff)
+apply (metis diff_Suc_Suc nat.cases(2) nth.simps zero_less_diff)
done
lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"