diff -r f0fc8531c909 -r cab4f808f791 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Dec 06 16:56:00 2007 +0100
+++ b/src/HOL/List.thy	Thu Dec 06 17:05:44 2007 +0100
@@ -109,6 +109,7 @@
 where
   append_Nil:"[] @ ys = ys"
   | append_Cons: "(x#xs) @ ys = x # xs @ ys"
+declare append.simps [code]
 
 primrec
   "rev([]) = []"
@@ -3177,6 +3178,7 @@
 where 
   "x mem [] \<longleftrightarrow> False"
   | "x mem (y#ys) \<longleftrightarrow> (if y = x then True else x mem ys)"
+declare member.simps [code]
 
 primrec
   "null [] = True"