diff -r 056255ade52a -r 4e74209f113e src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Int.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -24,7 +24,7 @@
 definition
   intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set"
 where
-  [code func del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
+  [code del]: "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
 
 typedef (Integ)
   int = "UNIV//intrel"
@@ -34,34 +34,34 @@
 begin
 
 definition
-  Zero_int_def [code func del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
+  Zero_int_def [code del]: "0 = Abs_Integ (intrel `` {(0, 0)})"
 
 definition
-  One_int_def [code func del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
+  One_int_def [code del]: "1 = Abs_Integ (intrel `` {(1, 0)})"
 
 definition
-  add_int_def [code func del]: "z + w = Abs_Integ
+  add_int_def [code del]: "z + w = Abs_Integ
     (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u, v) \<in> Rep_Integ w.
       intrel `` {(x + u, y + v)})"
 
 definition
-  minus_int_def [code func del]:
+  minus_int_def [code del]:
     "- z = Abs_Integ (\<Union>(x, y) \<in> Rep_Integ z. intrel `` {(y, x)})"
 
 definition
-  diff_int_def [code func del]:  "z - w = z + (-w \<Colon> int)"
+  diff_int_def [code del]:  "z - w = z + (-w \<Colon> int)"
 
 definition
-  mult_int_def [code func del]: "z * w = Abs_Integ
+  mult_int_def [code del]: "z * w = Abs_Integ
     (\<Union>(x, y) \<in> Rep_Integ z. \<Union>(u,v ) \<in> Rep_Integ w.
       intrel `` {(x*u + y*v, x*v + y*u)})"
 
 definition
-  le_int_def [code func del]:
+  le_int_def [code del]:
    "z \<le> w \<longleftrightarrow> (\<exists>x y u v. x+v \<le> u+y \<and> (x, y) \<in> Rep_Integ z \<and> (u, v) \<in> Rep_Integ w)"
 
 definition
-  less_int_def [code func del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
+  less_int_def [code del]: "(z\<Colon>int) < w \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
 
 definition
   zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
@@ -298,7 +298,7 @@
 definition
   of_int :: "int \<Rightarrow> 'a"
 where
-  [code func del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
+  [code del]: "of_int z = contents (\<Union>(i, j) \<in> Rep_Integ z. { of_nat i - of_nat j })"
 
 lemma of_int: "of_int (Abs_Integ (intrel `` {(i,j)})) = of_nat i - of_nat j"
 proof -
@@ -390,7 +390,7 @@
 definition
   nat :: "int \<Rightarrow> nat"
 where
-  [code func del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
+  [code del]: "nat z = contents (\<Union>(x, y) \<in> Rep_Integ z. {x-y})"
 
 lemma nat: "nat (Abs_Integ (intrel``{(x,y)})) = x-y"
 proof -
@@ -585,19 +585,19 @@
 
 definition
   Pls :: int where
-  [code func del]: "Pls = 0"
+  [code del]: "Pls = 0"
 
 definition
   Min :: int where
-  [code func del]: "Min = - 1"
+  [code del]: "Min = - 1"
 
 definition
   Bit0 :: "int \<Rightarrow> int" where
-  [code func del]: "Bit0 k = k + k"
+  [code del]: "Bit0 k = k + k"
 
 definition
   Bit1 :: "int \<Rightarrow> int" where
-  [code func del]: "Bit1 k = 1 + k + k"
+  [code del]: "Bit1 k = 1 + k + k"
 
 class number = type + -- {* for numeric types: nat, int, real, \dots *}
   fixes number_of :: "int \<Rightarrow> 'a"
@@ -622,11 +622,11 @@
 
 definition
   succ :: "int \<Rightarrow> int" where
-  [code func del]: "succ k = k + 1"
+  [code del]: "succ k = k + 1"
 
 definition
   pred :: "int \<Rightarrow> int" where
-  [code func del]: "pred k = k - 1"
+  [code del]: "pred k = k - 1"
 
 lemmas
   max_number_of [simp] = max_def
@@ -785,7 +785,7 @@
 begin
 
 definition
-  int_number_of_def [code func del]: "number_of w = (of_int w \<Colon> int)"
+  int_number_of_def [code del]: "number_of w = (of_int w \<Colon> int)"
 
 instance
   by intro_classes (simp only: int_number_of_def)
@@ -1167,7 +1167,7 @@
 definition
   Ints  :: "'a set"
 where
-  [code func del]: "Ints = range of_int"
+  [code del]: "Ints = range of_int"
 
 end
 
@@ -1799,36 +1799,36 @@
 
 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
 
-lemmas pred_succ_numeral_code [code func] =
+lemmas pred_succ_numeral_code [code] =
   pred_bin_simps succ_bin_simps
 
-lemmas plus_numeral_code [code func] =
+lemmas plus_numeral_code [code] =
   add_bin_simps
   arith_extra_simps(1) [where 'a = int]
 
-lemmas minus_numeral_code [code func] =
+lemmas minus_numeral_code [code] =
   minus_bin_simps
   arith_extra_simps(2) [where 'a = int]
   arith_extra_simps(5) [where 'a = int]
 
-lemmas times_numeral_code [code func] =
+lemmas times_numeral_code [code] =
   mult_bin_simps
   arith_extra_simps(4) [where 'a = int]
 
 instantiation int :: eq
 begin
 
-definition [code func del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
+definition [code del]: "eq_class.eq k l \<longleftrightarrow> k - l = (0\<Colon>int)"
 
 instance by default (simp add: eq_int_def)
 
 end
 
-lemma eq_number_of_int_code [code func]:
+lemma eq_number_of_int_code [code]:
   "eq_class.eq (number_of k \<Colon> int) (number_of l) \<longleftrightarrow> eq_class.eq k l"
   unfolding eq_int_def number_of_is_id ..
 
-lemma eq_int_code [code func]:
+lemma eq_int_code [code]:
   "eq_class.eq Int.Pls Int.Pls \<longleftrightarrow> True"
   "eq_class.eq Int.Pls Int.Min \<longleftrightarrow> False"
   "eq_class.eq Int.Pls (Int.Bit0 k2) \<longleftrightarrow> eq_class.eq Int.Pls k2"
@@ -1859,11 +1859,11 @@
   "eq_class.eq (k::int) k \<longleftrightarrow> True"
   by (rule HOL.eq_refl)
 
-lemma less_eq_number_of_int_code [code func]:
+lemma less_eq_number_of_int_code [code]:
   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
   unfolding number_of_is_id ..
 
-lemma less_eq_int_code [code func]:
+lemma less_eq_int_code [code]:
   "Int.Pls \<le> Int.Pls \<longleftrightarrow> True"
   "Int.Pls \<le> Int.Min \<longleftrightarrow> False"
   "Int.Pls \<le> Int.Bit0 k \<longleftrightarrow> Int.Pls \<le> k"
@@ -1890,11 +1890,11 @@
     (auto simp add: neg_def linorder_not_less group_simps
       zle_add1_eq_le [symmetric] del: iffI , auto simp only: Bit0_def Bit1_def)
 
-lemma less_number_of_int_code [code func]:
+lemma less_number_of_int_code [code]:
   "(number_of k \<Colon> int) < number_of l \<longleftrightarrow> k < l"
   unfolding number_of_is_id ..
 
-lemma less_int_code [code func]:
+lemma less_int_code [code]:
   "Int.Pls < Int.Pls \<longleftrightarrow> False"
   "Int.Pls < Int.Min \<longleftrightarrow> False"
   "Int.Pls < Int.Bit0 k \<longleftrightarrow> Int.Pls < k"
@@ -1935,11 +1935,11 @@
 
 hide (open) const nat_aux
 
-lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
+lemma zero_is_num_zero [code, code inline, symmetric, code post]:
   "(0\<Colon>int) = Numeral0" 
   by simp
 
-lemma one_is_num_one [code func, code inline, symmetric, code post]:
+lemma one_is_num_one [code, code inline, symmetric, code post]:
   "(1\<Colon>int) = Numeral1" 
   by simp