src/HOL/List.thy

--- a/src/HOL/List.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/List.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -109,7 +109,6 @@
 where
   append_Nil:"[] @ ys = ys"
   | append_Cons: "(x#xs) @ ys = x # xs @ ys"
-declare append.simps [code]
 
 primrec
   "rev([]) = []"
@@ -2691,9 +2690,16 @@
 
 text{* The integers are an instance of the above class: *}
 
-instance int:: finite_intvl_succ
-  successor_int_def: "successor == (%i\<Colon>int. i+1)"
-by intro_classes (simp_all add: successor_int_def)
+instantiation int:: finite_intvl_succ
+begin
+
+definition
+  successor_int_def: "successor = (%i\<Colon>int. i+1)"
+
+instance
+  by intro_classes (simp_all add: successor_int_def)
+
+end
 
 text{* Now @{term"[i..j::int]"} is defined for integers. *}
 
@@ -3178,7 +3184,6 @@
 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"