--- a/src/HOL/List.thy Sun Nov 20 21:07:06 2011 +0100
+++ b/src/HOL/List.thy Sun Nov 20 21:07:10 2011 +0100
@@ -2564,7 +2564,7 @@
-- {* simp does not terminate! *}
by (induct j) auto
-lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n", standard]
+lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n"] for m n
lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
by (subst upt_rec) simp
@@ -2679,9 +2679,9 @@
lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
by (cases n) simp_all
-lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]
-lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]
-lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]
+lemmas take_Cons_number_of = take_Cons'[of "number_of v"] for v
+lemmas drop_Cons_number_of = drop_Cons'[of "number_of v"] for v
+lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v"] for v
declare take_Cons_number_of [simp]
drop_Cons_number_of [simp]
@@ -2700,8 +2700,7 @@
declare upto.simps[code, simp del]
-lemmas upto_rec_number_of[simp] =
- upto.simps[of "number_of m" "number_of n", standard]
+lemmas upto_rec_number_of[simp] = upto.simps[of "number_of m" "number_of n"] for m n
lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
by(simp add: upto.simps)