--- a/src/HOL/List.thy Mon Nov 06 16:28:33 2006 +0100
+++ b/src/HOL/List.thy Mon Nov 06 16:28:34 2006 +0100
@@ -2816,7 +2816,7 @@
lemmas list_bex_code [code unfold] =
list_ex_iff [symmetric, THEN eq_reflection]
-lemma itrev [simp, normal post]:
+lemma itrev [simp]:
"itrev xs ys = rev xs @ ys"
by (induct xs arbitrary: ys) simp_all
@@ -2828,7 +2828,7 @@
"map_filter f P xs = map f (filter P xs)"
by (induct xs) auto
-lemma rev_code [code func, code unfold]:
+lemma rev_code [code func, code unfold, code noinline]:
"rev xs == itrev xs []"
by simp