# HG changeset patch
# User haftmann
# Date 1223613953 -7200
# Node ID 4e74209f113e4e1f8970432d95fce081f350102c
# Parent  056255ade52a732f295ddc6889bd3dd3e4341244
`code func` now just `code`

diff -r 056255ade52a -r 4e74209f113e doc-src/IsarAdvanced/Codegen/Thy/Program.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Program.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Program.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -25,7 +25,7 @@
   explicitly:
 *}
 
-lemma %quoteme [code func]:
+lemma %quoteme [code]:
   "dequeue (Queue xs []) =
      (if xs = [] then (None, Queue [] [])
        else dequeue (Queue [] (rev xs)))"
@@ -34,7 +34,7 @@
   by (cases xs, simp_all) (cases "rev xs", simp_all)
 
 text {*
-  \noindent The annotation @{text "[code func]"} is an @{text Isar}
+  \noindent The annotation @{text "[code]"} is an @{text Isar}
   @{text attribute} which states that the given theorems should be
   considered as defining equations for a @{text fun} statement --
   the corresponding constant is determined syntactically.  The resulting code:
@@ -255,7 +255,7 @@
   the operations, e.g. @{term "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat"}:
 *}
 
-lemma %quoteme plus_Dig [code func]:
+lemma %quoteme plus_Dig [code]:
   "0 + n = n"
   "m + 0 = m"
   "1 + Dig0 n = Dig1 n"
@@ -282,12 +282,12 @@
   which are an obstacle here:
 *}
 
-lemma %quoteme Suc_Dig [code func]:
+lemma %quoteme Suc_Dig [code]:
   "Suc n = n + 1"
   by simp
 
 declare %quoteme One_nat_def [code inline del]
-declare %quoteme add_Suc_shift [code func del] 
+declare %quoteme add_Suc_shift [code del] 
 
 text {*
   \noindent This yields the following code:
@@ -316,10 +316,10 @@
 *}
 
 code_datatype %invisible "0::nat" Suc
-declare %invisible plus_Dig [code func del]
+declare %invisible plus_Dig [code del]
 declare %invisible One_nat_def [code inline]
-declare %invisible add_Suc_shift [code func] 
-lemma %invisible [code func]: "0 + n = (n \<Colon> nat)" by simp
+declare %invisible add_Suc_shift [code] 
+lemma %invisible [code]: "0 + n = (n \<Colon> nat)" by simp
 
 
 subsection {* Equality and wellsortedness *}
@@ -367,10 +367,10 @@
 instantiation %quoteme "*" :: (order, order) order
 begin
 
-definition %quoteme [code func del]:
+definition %quoteme [code del]:
   "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
 
-definition %quoteme [code func del]:
+definition %quoteme [code del]:
   "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
 
 instance %quoteme proof
@@ -378,7 +378,7 @@
 
 end %quoteme
 
-lemma %quoteme order_prod [code func]:
+lemma %quoteme order_prod [code]:
   "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
      x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
   "(x1 \<Colon> 'a\<Colon>order, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
@@ -396,7 +396,7 @@
   code theorems:
 *}
 
-lemma %quoteme order_prod_code [code func]:
+lemma %quoteme order_prod_code [code]:
   "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) < (x2, y2) \<longleftrightarrow>
      x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
   "(x1 \<Colon> 'a\<Colon>{order, eq}, y1 \<Colon> 'b\<Colon>order) \<le> (x2, y2) \<longleftrightarrow>
@@ -438,7 +438,7 @@
   @{const [show_types] list_all2} can do the job:
 *}
 
-lemma %quoteme monotype_eq_list_all2 [code func]:
+lemma %quoteme monotype_eq_list_all2 [code]:
   "eq_class.eq (Mono tyco1 typargs1) (Mono tyco2 typargs2) \<longleftrightarrow>
      eq_class.eq tyco1 tyco2 \<and> list_all2 eq_class.eq typargs1 typargs2"
   by (simp add: eq list_all2_eq [symmetric])
diff -r 056255ade52a -r 4e74209f113e doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex
--- a/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Fri Oct 10 06:45:50 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Program.tex	Fri Oct 10 06:45:53 2008 +0200
@@ -55,7 +55,7 @@
 %
 \isatagquoteme
 \isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
 \ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
 \ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
@@ -71,7 +71,7 @@
 \endisadelimquoteme
 %
 \begin{isamarkuptext}%
-\noindent The annotation \isa{{\isacharbrackleft}code\ func{\isacharbrackright}} is an \isa{Isar}
+\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}
   \isa{attribute} which states that the given theorems should be
   considered as defining equations for a \isa{fun} statement --
   the corresponding constant is determined syntactically.  The resulting code:%
@@ -287,8 +287,8 @@
 \verb|};|\newline%
 \newline%
 \verb|pow :: forall a. (Monoid a) => Nat -> a -> a;|\newline%
+\verb|pow Zero_nat a = neutral;|\newline%
 \verb|pow (Suc n) a = mult a (pow n a);|\newline%
-\verb|pow Zero_nat a = neutral;|\newline%
 \newline%
 \verb|plus_nat :: Nat -> Nat -> Nat;|\newline%
 \verb|plus_nat (Suc m) n = plus_nat m (Suc n);|\newline%
@@ -298,8 +298,8 @@
 \verb|neutral_nat = Suc Zero_nat;|\newline%
 \newline%
 \verb|mult_nat :: Nat -> Nat -> Nat;|\newline%
+\verb|mult_nat Zero_nat n = Zero_nat;|\newline%
 \verb|mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline%
-\verb|mult_nat Zero_nat n = Zero_nat;|\newline%
 \newline%
 \verb|instance Semigroup Nat where {|\newline%
 \verb|  mult = mult_nat;|\newline%
@@ -350,16 +350,16 @@
 \verb|fun semigroup_monoid (A_:'a monoid) = #Program__semigroup_monoid A_;|\newline%
 \verb|fun neutral (A_:'a monoid) = #neutral A_;|\newline%
 \newline%
-\verb|fun pow A_ (Suc n) a = mult (semigroup_monoid A_) a (pow A_ n a)|\newline%
-\verb|  |\verb,|,\verb| pow A_ Zero_nat a = neutral A_;|\newline%
+\verb|fun pow A_ Zero_nat a = neutral A_|\newline%
+\verb|  |\verb,|,\verb| pow A_ (Suc n) a = mult (semigroup_monoid A_) a (pow A_ n a);|\newline%
 \newline%
 \verb|fun plus_nat (Suc m) n = plus_nat m (Suc n)|\newline%
 \verb|  |\verb,|,\verb| plus_nat Zero_nat n = n;|\newline%
 \newline%
 \verb|val neutral_nat : nat = Suc Zero_nat;|\newline%
 \newline%
-\verb|fun mult_nat (Suc m) n = plus_nat n (mult_nat m n)|\newline%
-\verb|  |\verb,|,\verb| mult_nat Zero_nat n = Zero_nat;|\newline%
+\verb|fun mult_nat Zero_nat n = Zero_nat|\newline%
+\verb|  |\verb,|,\verb| mult_nat (Suc m) n = plus_nat n (mult_nat m n);|\newline%
 \newline%
 \verb|val semigroup_nat = {mult = mult_nat} : nat semigroup;|\newline%
 \newline%
@@ -575,7 +575,7 @@
 %
 \isatagquoteme
 \isacommand{lemma}\isamarkupfalse%
-\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
 \ \ {\isachardoublequoteopen}m\ {\isacharplus}\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharplus}\ Dig{\isadigit{0}}\ n\ {\isacharequal}\ Dig{\isadigit{1}}\ n{\isachardoublequoteclose}\isanewline
@@ -629,7 +629,7 @@
 %
 \isatagquoteme
 \isacommand{lemma}\isamarkupfalse%
-\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ Suc{\isacharunderscore}Dig\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}Suc\ n\ {\isacharequal}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%
 \ simp\isanewline
@@ -637,7 +637,7 @@
 \isacommand{declare}\isamarkupfalse%
 \ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline\ del{\isacharbrackright}\isanewline
 \isacommand{declare}\isamarkupfalse%
-\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}%
+\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ del{\isacharbrackright}%
 \endisatagquoteme
 {\isafoldquoteme}%
 %
@@ -715,13 +715,13 @@
 \isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
 \ {\isachardoublequoteopen}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isachardoublequoteclose}\ Suc\isanewline
 \isacommand{declare}\isamarkupfalse%
-\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}\isanewline
+\ plus{\isacharunderscore}Dig\ {\isacharbrackleft}code\ del{\isacharbrackright}\isanewline
 \isacommand{declare}\isamarkupfalse%
 \ One{\isacharunderscore}nat{\isacharunderscore}def\ {\isacharbrackleft}code\ inline{\isacharbrackright}\isanewline
 \isacommand{declare}\isamarkupfalse%
-\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code\ func{\isacharbrackright}\ \isanewline
+\ add{\isacharunderscore}Suc{\isacharunderscore}shift\ {\isacharbrackleft}code{\isacharbrackright}\ \isanewline
 \isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isacharplus}\ n\ {\isacharequal}\ {\isacharparenleft}n\ {\isasymColon}\ nat{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ simp%
 \endisataginvisible
 {\isafoldinvisible}%
@@ -784,15 +784,15 @@
 \newline%
 \verb|fun eqop A_ a b = eq A_ a b;|\newline%
 \newline%
-\verb|fun member A_ x (y :: ys) = eqop A_ x y orelse member A_ x ys|\newline%
-\verb|  |\verb,|,\verb| member A_ x [] = false;|\newline%
+\verb|fun member A_ x [] = false|\newline%
+\verb|  |\verb,|,\verb| member A_ x (y :: ys) = eqop A_ x y orelse member A_ x ys;|\newline%
 \newline%
-\verb|fun collect_duplicates A_ xs ys (z :: zs) =|\newline%
-\verb|  (if member A_ z xs|\newline%
-\verb|    then (if member A_ z ys then collect_duplicates A_ xs ys zs|\newline%
-\verb|           else collect_duplicates A_ xs (z :: ys) zs)|\newline%
-\verb|    else collect_duplicates A_ (z :: xs) (z :: ys) zs)|\newline%
-\verb|  |\verb,|,\verb| collect_duplicates A_ xs ys [] = xs;|\newline%
+\verb|fun collect_duplicates A_ xs ys [] = xs|\newline%
+\verb|  |\verb,|,\verb| collect_duplicates A_ xs ys (z :: zs) =|\newline%
+\verb|    (if member A_ z xs|\newline%
+\verb|      then (if member A_ z ys then collect_duplicates A_ xs ys zs|\newline%
+\verb|             else collect_duplicates A_ xs (z :: ys) zs)|\newline%
+\verb|      else collect_duplicates A_ (z :: xs) (z :: ys) zs);|\newline%
 \newline%
 \verb|end; (*struct Example*)|%
 \end{isamarkuptext}%
@@ -835,11 +835,11 @@
 \isakeyword{begin}\isanewline
 \isanewline
 \isacommand{definition}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}x\ {\isasymle}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isasymle}\ snd\ y{\isachardoublequoteclose}\isanewline
 \isanewline
 \isacommand{definition}\isamarkupfalse%
-\ {\isacharbrackleft}code\ func\ del{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code\ del{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}x\ {\isacharless}\ y\ {\isasymlongleftrightarrow}\ fst\ x\ {\isacharless}\ fst\ y\ {\isasymor}\ fst\ x\ {\isacharequal}\ fst\ y\ {\isasymand}\ snd\ x\ {\isacharless}\ snd\ y{\isachardoublequoteclose}\isanewline
 \isanewline
 \isacommand{instance}\isamarkupfalse%
@@ -852,7 +852,7 @@
 \isanewline
 \isanewline
 \isacommand{lemma}\isamarkupfalse%
-\ order{\isacharunderscore}prod\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ order{\isacharunderscore}prod\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}order{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
@@ -884,7 +884,7 @@
 %
 \isatagquoteme
 \isacommand{lemma}\isamarkupfalse%
-\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ order{\isacharunderscore}prod{\isacharunderscore}code\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
 \ \ \ \ \ x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}\ {\isasymor}\ x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}\ {\isasymand}\ y{\isadigit{1}}\ {\isacharless}\ y{\isadigit{2}}{\isachardoublequoteclose}\isanewline
 \ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}a{\isasymColon}{\isacharbraceleft}order{\isacharcomma}\ eq{\isacharbraceright}{\isacharcomma}\ y{\isadigit{1}}\ {\isasymColon}\ {\isacharprime}b{\isasymColon}order{\isacharparenright}\ {\isasymle}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
@@ -1007,7 +1007,7 @@
 %
 \isatagquoteme
 \isacommand{lemma}\isamarkupfalse%
-\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code\ func{\isacharbrackright}{\isacharcolon}\isanewline
+\ monotype{\isacharunderscore}eq{\isacharunderscore}list{\isacharunderscore}all{\isadigit{2}}\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}eq{\isacharunderscore}class{\isachardot}eq\ {\isacharparenleft}Mono\ tyco{\isadigit{1}}\ typargs{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}Mono\ tyco{\isadigit{2}}\ typargs{\isadigit{2}}{\isacharparenright}\ {\isasymlongleftrightarrow}\isanewline
 \ \ \ \ \ eq{\isacharunderscore}class{\isachardot}eq\ tyco{\isadigit{1}}\ tyco{\isadigit{2}}\ {\isasymand}\ list{\isacharunderscore}all{\isadigit{2}}\ eq{\isacharunderscore}class{\isachardot}eq\ typargs{\isadigit{1}}\ typargs{\isadigit{2}}{\isachardoublequoteclose}\isanewline
 \ \ \isacommand{by}\isamarkupfalse%
@@ -1038,8 +1038,8 @@
 \newline%
 \verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
 \newline%
-\verb|fun null (x :: xs) = false|\newline%
-\verb|  |\verb,|,\verb| null [] = true;|\newline%
+\verb|fun null [] = true|\newline%
+\verb|  |\verb,|,\verb| null (x :: xs) = false;|\newline%
 \newline%
 \verb|fun eq_nat (Suc a) Zero_nat = false|\newline%
 \verb|  |\verb,|,\verb| eq_nat Zero_nat (Suc a) = false|\newline%
diff -r 056255ade52a -r 4e74209f113e doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -993,7 +993,7 @@
     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     ;
 
-    'code' ('func' | 'inline') ( 'del' )?
+    'code' ( 'inline' ) ? ( 'del' ) ?
     ;
   \end{rail}
 
@@ -1080,13 +1080,13 @@
   are not required to have a definition by means of defining equations;
   if needed these are implemented by program abort instead.
 
-  \item [@{attribute (HOL) code}~@{text func}] explicitly selects (or
-  with option ``@{text "del:"}'' deselects) a defining equation for
+  \item [@{attribute (HOL) code}] explicitly selects (or
+  with option ``@{text "del"}'' deselects) a defining equation for
   code generation.  Usually packages introducing defining equations
   provide a reasonable default setup for selection.
 
   \item [@{attribute (HOL) code}@{text inline}] declares (or with
-  option ``@{text "del:"}'' removes) inlining theorems which are
+  option ``@{text "del"}'' removes) inlining theorems which are
   applied as rewrite rules to any defining equation during
   preprocessing.
 
diff -r 056255ade52a -r 4e74209f113e doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 10 06:45:50 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 10 06:45:53 2008 +0200
@@ -997,7 +997,7 @@
     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     ;
 
-    'code' ('func' | 'inline') ( 'del' )?
+    'code' ( 'inline' ) ? ( 'del' ) ?
     ;
   \end{rail}
 
@@ -1081,13 +1081,13 @@
   are not required to have a definition by means of defining equations;
   if needed these are implemented by program abort instead.
 
-  \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{func}] explicitly selects (or
-  with option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' deselects) a defining equation for
+  \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}] explicitly selects (or
+  with option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a defining equation for
   code generation.  Usually packages introducing defining equations
   provide a reasonable default setup for selection.
 
   \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}\isa{inline}] declares (or with
-  option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' removes) inlining theorems which are
+  option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
   applied as rewrite rules to any defining equation during
   preprocessing.
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Code_Eval.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -133,14 +133,14 @@
 
 subsubsection {* Code generator setup *}
 
-lemmas [code func del] = term.recs term.cases term.size
-lemma [code func, code func del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
+lemmas [code del] = term.recs term.cases term.size
+lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
 
-lemma [code func, code func del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
-lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
-lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
+lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
+lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
+lemma [code, code del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
 
-lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code func]: "Code_Eval.term_of c =
+lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code]: "Code_Eval.term_of c =
     (let (n, m) = nibble_pair_of_char c
   in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
     (Code_Eval.term_of n)) (Code_Eval.term_of m))"
diff -r 056255ade52a -r 4e74209f113e src/HOL/Code_Setup.thy
--- a/src/HOL/Code_Setup.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Code_Setup.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -21,32 +21,32 @@
 
 text {* Code equations *}
 
-lemma [code func]:
+lemma [code]:
   shows "False \<and> x \<longleftrightarrow> False"
     and "True \<and> x \<longleftrightarrow> x"
     and "x \<and> False \<longleftrightarrow> False"
     and "x \<and> True \<longleftrightarrow> x" by simp_all
 
-lemma [code func]:
+lemma [code]:
   shows "False \<or> x \<longleftrightarrow> x"
     and "True \<or> x \<longleftrightarrow> True"
     and "x \<or> False \<longleftrightarrow> x"
     and "x \<or> True \<longleftrightarrow> True" by simp_all
 
-lemma [code func]:
+lemma [code]:
   shows "\<not> True \<longleftrightarrow> False"
     and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
 
-lemmas [code func] = Let_def if_True if_False
+lemmas [code] = Let_def if_True if_False
 
-lemmas [code func, code unfold, symmetric, code post] = imp_conv_disj
+lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
 
 text {* Equality *}
 
 context eq
 begin
 
-lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
+lemma equals_eq [code inline, code]: "op = \<equiv> eq"
   by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
 
 declare eq [code unfold, code inline del]
diff -r 056255ade52a -r 4e74209f113e src/HOL/Complex/ex/ReflectedFerrack.thy
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -481,7 +481,7 @@
   "numgcdh (C i) = (\<lambda>g. zgcd i g)"
   "numgcdh (CN n c t) = (\<lambda>g. zgcd c (numgcdh t g))"
   "numgcdh t = (\<lambda>g. 1)"
-defs numgcd_def [code func]: "numgcd t \<equiv> numgcdh t (maxcoeff t)"
+defs numgcd_def [code]: "numgcd t \<equiv> numgcdh t (maxcoeff t)"
 
 recdef reducecoeffh "measure size"
   "reducecoeffh (C i) = (\<lambda> g. C (i div g))"
diff -r 056255ade52a -r 4e74209f113e src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Datatype.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -635,7 +635,7 @@
 definition
   option_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"
 where
-  [code func del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
+  [code del]: "option_map = (%f y. case y of None => None | Some x => Some (f x))"
 
 lemma option_map_None [simp, code]: "option_map f None = None"
   by (simp add: option_map_def)
diff -r 056255ade52a -r 4e74209f113e src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Divides.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -127,7 +127,7 @@
   note that ultimately show thesis by blast
 qed
 
-lemma dvd_eq_mod_eq_0 [code func]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
 proof
   assume "b mod a = 0"
   with mod_div_equality [of b a] have "b div a * a = b" by simp
@@ -230,7 +230,7 @@
 begin
 
 definition divmod :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where
-  [code func del]: "divmod m n = (THE (q, r). divmod_rel m n q r)"
+  [code del]: "divmod m n = (THE (q, r). divmod_rel m n q r)"
 
 definition div_nat where
   "m div n = fst (divmod m n)"
diff -r 056255ade52a -r 4e74209f113e src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Equiv_Relations.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -94,7 +94,7 @@
 subsection {* Quotients *}
 
 definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"  (infixl "'/'/" 90) where
-  [code func del]: "A//r = (\<Union>x \<in> A. {r``{x}})"  -- {* set of equiv classes *}
+  [code del]: "A//r = (\<Union>x \<in> A. {r``{x}})"  -- {* set of equiv classes *}
 
 lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r"
   by (unfold quotient_def) blast
diff -r 056255ade52a -r 4e74209f113e src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Fun.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -117,7 +117,7 @@
 
 definition
   bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
-  [code func del]: "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
+  [code del]: "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
 
 constdefs
   surj :: "('a => 'b) => bool"                   (*surjective*)
diff -r 056255ade52a -r 4e74209f113e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/HOL.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -1227,7 +1227,7 @@
 
 constdefs
   simp_implies :: "[prop, prop] => prop"  (infixr "=simp=>" 1)
-  [code func del]: "simp_implies \<equiv> op ==>"
+  [code del]: "simp_implies \<equiv> op ==>"
 
 lemma simp_impliesI:
   assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
diff -r 056255ade52a -r 4e74209f113e src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Hyperreal/Integration.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -16,29 +16,29 @@
   --{*Partitions and tagged partitions etc.*}
 
   partition :: "[(real*real),nat => real] => bool" where
-  [code func del]: "partition = (%(a,b) D. D 0 = a &
+  [code del]: "partition = (%(a,b) D. D 0 = a &
                          (\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) &
                               (\<forall>n \<ge> N. D(n) = b)))"
 
 definition
   psize :: "(nat => real) => nat" where
-  [code func del]:"psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
+  [code del]:"psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
                       (\<forall>n \<ge> N. D(n) = D(N)))"
 
 definition
   tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool" where
-  [code func del]:"tpart = (%(a,b) (D,p). partition(a,b) D &
+  [code del]:"tpart = (%(a,b) (D,p). partition(a,b) D &
                           (\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n)))"
 
   --{*Gauges and gauge-fine divisions*}
 
 definition
   gauge :: "[real => bool, real => real] => bool" where
-  [code func del]:"gauge E g = (\<forall>x. E x --> 0 < g(x))"
+  [code del]:"gauge E g = (\<forall>x. E x --> 0 < g(x))"
 
 definition
   fine :: "[real => real, ((nat => real)*(nat => real))] => bool" where
-  [code func del]:"fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
+  [code del]:"fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
 
   --{*Riemann sum*}
 
@@ -50,7 +50,7 @@
 
 definition
   Integral :: "[(real*real),real=>real,real] => bool" where
-  [code func del]: "Integral = (%(a,b) f k. \<forall>e > 0.
+  [code del]: "Integral = (%(a,b) f k. \<forall>e > 0.
                                (\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
                                (\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
                                          \<bar>rsum(D,p) f - k\<bar> < e)))"
diff -r 056255ade52a -r 4e74209f113e src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -16,7 +16,7 @@
 definition
   LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
         ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
-  [code func del]: "f -- a --> L =
+  [code del]: "f -- a --> L =
      (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s
         --> norm (f x - L) < r)"
 
@@ -26,7 +26,7 @@
 
 definition
   isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
-  [code func del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
+  [code del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
 
 
 subsection {* Limits of Functions *}
diff -r 056255ade52a -r 4e74209f113e src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -15,13 +15,13 @@
 definition
   Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where
     --{*Standard definition of sequence converging to zero*}
-  [code func del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
+  [code del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
 
 definition
   LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
     ("((_)/ ----> (_))" [60, 60] 60) where
     --{*Standard definition of convergence of sequence*}
-  [code func del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
+  [code del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
 
 definition
   lim :: "(nat => 'a::real_normed_vector) => 'a" where
@@ -36,22 +36,22 @@
 definition
   Bseq :: "(nat => 'a::real_normed_vector) => bool" where
     --{*Standard definition for bounded sequence*}
-  [code func del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
+  [code del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
 
 definition
   monoseq :: "(nat=>real)=>bool" where
     --{*Definition for monotonicity*}
-  [code func del]: "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
+  [code del]: "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
 
 definition
   subseq :: "(nat => nat) => bool" where
     --{*Definition of subsequence*}
-  [code func del]:   "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
+  [code del]:   "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
 
 definition
   Cauchy :: "(nat => 'a::real_normed_vector) => bool" where
     --{*Standard definition of the Cauchy condition*}
-  [code func del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
+  [code del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
 
 
 subsection {* Bounded Sequences *}
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
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/IntDiv.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -14,13 +14,13 @@
 constdefs
   quorem :: "(int*int) * (int*int) => bool"
     --{*definition of quotient and remainder*}
-    [code func]: "quorem == %((a,b), (q,r)).
+    [code]: "quorem == %((a,b), (q,r)).
                       a = b*q + r &
                       (if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)"
 
   adjust :: "[int, int*int] => int*int"
     --{*for the division algorithm*}
-    [code func]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
+    [code]: "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
                          else (2*q, r)"
 
 text{*algorithm for the case @{text "a\<ge>0, b>0"}*}
@@ -46,7 +46,7 @@
 text{*algorithm for the general case @{term "b\<noteq>0"}*}
 constdefs
   negateSnd :: "int*int => int*int"
-    [code func]: "negateSnd == %(q,r). (q,-r)"
+    [code]: "negateSnd == %(q,r). (q,-r)"
 
 definition
   divAlg :: "int \<times> int \<Rightarrow> int \<times> int"
@@ -1477,7 +1477,7 @@
 context ring_1
 begin
 
-lemma of_int_num [code func]:
+lemma of_int_num [code]:
   "of_int k = (if k = 0 then 0 else if k < 0 then
      - of_int (- k) else let
        (l, m) = divAlg (k, 2);
diff -r 056255ade52a -r 4e74209f113e src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Lattices.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -9,7 +9,7 @@
 imports Fun
 begin
 
-subsection{* Lattices *}
+subsection {* Lattices *}
 
 notation
   less_eq  (infix "\<sqsubseteq>" 50) and
@@ -40,7 +40,7 @@
 class lattice = lower_semilattice + upper_semilattice
 
 
-subsubsection{* Intro and elim rules*}
+subsubsection {* Intro and elim rules*}
 
 context lower_semilattice
 begin
@@ -512,10 +512,10 @@
 begin
 
 definition
-  inf_fun_eq [code func del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
+  inf_fun_eq [code del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
 
 definition
-  sup_fun_eq [code func del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
+  sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
 
 instance
 apply intro_classes
@@ -536,10 +536,10 @@
 begin
 
 definition
-  Inf_fun_def [code func del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
+  Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
 
 definition
-  Sup_fun_def [code func del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
+  Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
 
 instance
   by intro_classes
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Array.thy
--- a/src/HOL/Library/Array.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Array.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -107,14 +107,14 @@
 
 subsection {* Properties *}
 
-lemma array_make [code func]:
+lemma array_make [code]:
   "Array.new n x = make n (\<lambda>_. x)"
   by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def
     monad_simp array_of_list_replicate [symmetric]
     map_replicate_trivial replicate_append_same
     of_list_def)
 
-lemma array_of_list_make [code func]:
+lemma array_of_list_make [code]:
   "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
   unfolding make_def map_nth ..
 
@@ -126,28 +126,28 @@
 definition new' where
   [code del]: "new' = Array.new o nat_of_index"
 hide (open) const new'
-lemma [code func]:
+lemma [code]:
   "Array.new = Array.new' o index_of_nat"
   by (simp add: new'_def o_def)
 
 definition of_list' where
   [code del]: "of_list' i xs = Array.of_list (take (nat_of_index i) xs)"
 hide (open) const of_list'
-lemma [code func]:
+lemma [code]:
   "Array.of_list xs = Array.of_list' (index_of_nat (List.length xs)) xs"
   by (simp add: of_list'_def)
 
 definition make' where
   [code del]: "make' i f = Array.make (nat_of_index i) (f o index_of_nat)"
 hide (open) const make'
-lemma [code func]:
+lemma [code]:
   "Array.make n f = Array.make' (index_of_nat n) (f o nat_of_index)"
   by (simp add: make'_def o_def)
 
 definition length' where
   [code del]: "length' = Array.length \<guillemotright>== liftM index_of_nat"
 hide (open) const length'
-lemma [code func]:
+lemma [code]:
   "Array.length = Array.length' \<guillemotright>== liftM nat_of_index"
   by (simp add: length'_def monad_simp',
     simp add: liftM_def comp_def monad_simp,
@@ -156,14 +156,14 @@
 definition nth' where
   [code del]: "nth' a = Array.nth a o nat_of_index"
 hide (open) const nth'
-lemma [code func]:
+lemma [code]:
   "Array.nth a n = Array.nth' a (index_of_nat n)"
   by (simp add: nth'_def)
 
 definition upd' where
   [code del]: "upd' a i x = Array.upd (nat_of_index i) x a \<guillemotright> return ()"
 hide (open) const upd'
-lemma [code func]:
+lemma [code]:
   "Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a"
   by (simp add: upd'_def monad_simp upd_return)
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Char_nat.thy
--- a/src/HOL/Library/Char_nat.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Char_nat.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -54,7 +54,7 @@
   "nibble_of_nat (n mod 16) = nibble_of_nat n"
   unfolding nibble_of_nat_def Let_def by auto
 
-lemmas [code func] = nibble_of_nat_norm [symmetric]
+lemmas [code] = nibble_of_nat_norm [symmetric]
 
 lemma nibble_of_nat_simps [simp]:
   "nibble_of_nat  0 = Nibble0"
@@ -75,7 +75,7 @@
   "nibble_of_nat 15 = NibbleF"
   unfolding nibble_of_nat_def Let_def by auto
 
-lemmas nibble_of_nat_code [code func] = nibble_of_nat_simps
+lemmas nibble_of_nat_code [code] = nibble_of_nat_simps
   [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc]
 
 lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
@@ -115,7 +115,7 @@
   nibble_pair_of_nat :: "nat \<Rightarrow> nibble \<times> nibble" where
   "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat (n mod 16))"
 
-lemma nibble_of_pair [code func]:
+lemma nibble_of_pair [code]:
   "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat n)"
   unfolding nibble_of_nat_norm [of n, symmetric] nibble_pair_of_nat_def ..
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Char_ord.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -64,11 +64,11 @@
 begin
 
 definition
-  char_less_eq_def [code func del]: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
+  char_less_eq_def [code del]: "c1 \<le> c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
     n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2)"
 
 definition
-  char_less_def [code func del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
+  char_less_def [code del]: "c1 < c2 \<longleftrightarrow> (case c1 of Char n1 m1 \<Rightarrow> case c2 of Char n2 m2 \<Rightarrow>
     n1 < n2 \<or> n1 = n2 \<and> m1 < m2)"
 
 instance
@@ -90,7 +90,7 @@
 
 end
 
-lemma [simp, code func]:
+lemma [simp, code]:
   shows char_less_eq_simp: "Char n1 m1 \<le> Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 \<le> m2"
   and char_less_simp:      "Char n1 m1 < Char n2 m2 \<longleftrightarrow> n1 < n2 \<or> n1 = n2 \<and> m1 < m2"
   unfolding char_less_eq_def char_less_def by simp_all
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Code_Char_chr.thy
--- a/src/HOL/Library/Code_Char_chr.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Code_Char_chr.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -12,28 +12,28 @@
 definition
   "int_of_char = int o nat_of_char"
 
-lemma [code func]:
+lemma [code]:
   "nat_of_char = nat o int_of_char"
   unfolding int_of_char_def by (simp add: expand_fun_eq)
 
 definition
   "char_of_int = char_of_nat o nat"
 
-lemma [code func]:
+lemma [code]:
   "char_of_nat = char_of_int o int"
   unfolding char_of_int_def by (simp add: expand_fun_eq)
 
-lemmas [code func del] = char.recs char.cases char.size
+lemmas [code del] = char.recs char.cases char.size
 
-lemma [code func, code inline]:
+lemma [code, code inline]:
   "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
   by (cases c) (auto simp add: nibble_pair_of_nat_char)
 
-lemma [code func, code inline]:
+lemma [code, code inline]:
   "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
   by (cases c) (auto simp add: nibble_pair_of_nat_char)
 
-lemma [code func]:
+lemma [code]:
   "size (c\<Colon>char) = 0"
   by (cases c) auto
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Code_Index.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -64,7 +64,7 @@
 instantiation index :: zero
 begin
 
-definition [simp, code func del]:
+definition [simp, code del]:
   "0 = index_of_nat 0"
 
 instance ..
@@ -87,12 +87,12 @@
   then show "P k" by simp
 qed simp_all
 
-lemmas [code func del] = index.recs index.cases
+lemmas [code del] = index.recs index.cases
 
 declare index_case [case_names nat, cases type: index]
 declare index.induct [case_names nat, induct type: index]
 
-lemma [code func]:
+lemma [code]:
   "index_size = nat_of_index"
 proof (rule ext)
   fix k
@@ -102,7 +102,7 @@
   finally show "index_size k = nat_of_index k" .
 qed
 
-lemma [code func]:
+lemma [code]:
   "size = nat_of_index"
 proof (rule ext)
   fix k
@@ -110,7 +110,7 @@
   by (induct k) (simp_all del: zero_index_def Suc_index_def, simp_all)
 qed
 
-lemma [code func]:
+lemma [code]:
   "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of_index k) (nat_of_index l)"
   by (cases k, cases l) (simp add: eq)
 
@@ -143,63 +143,63 @@
 instantiation index :: "{minus, ordered_semidom, Divides.div, linorder}"
 begin
 
-lemma zero_index_code [code inline, code func]:
+lemma zero_index_code [code inline, code]:
   "(0\<Colon>index) = Numeral0"
   by (simp add: number_of_index_def Pls_def)
 lemma [code post]: "Numeral0 = (0\<Colon>index)"
   using zero_index_code ..
 
-definition [simp, code func del]:
+definition [simp, code del]:
   "(1\<Colon>index) = index_of_nat 1"
 
-lemma one_index_code [code inline, code func]:
+lemma one_index_code [code inline, code]:
   "(1\<Colon>index) = Numeral1"
   by (simp add: number_of_index_def Pls_def Bit1_def)
 lemma [code post]: "Numeral1 = (1\<Colon>index)"
   using one_index_code ..
 
-definition [simp, code func del]:
+definition [simp, code del]:
   "n + m = index_of_nat (nat_of_index n + nat_of_index m)"
 
-lemma plus_index_code [code func]:
+lemma plus_index_code [code]:
   "index_of_nat n + index_of_nat m = index_of_nat (n + m)"
   by simp
 
-definition [simp, code func del]:
+definition [simp, code del]:
   "n - m = index_of_nat (nat_of_index n - nat_of_index m)"
 
-definition [simp, code func del]:
+definition [simp, code del]:
   "n * m = index_of_nat (nat_of_index n * nat_of_index m)"
 
-lemma times_index_code [code func]:
+lemma times_index_code [code]:
   "index_of_nat n * index_of_nat m = index_of_nat (n * m)"
   by simp
 
-definition [simp, code func del]:
+definition [simp, code del]:
   "n div m = index_of_nat (nat_of_index n div nat_of_index m)"
 
-definition [simp, code func del]:
+definition [simp, code del]:
   "n mod m = index_of_nat (nat_of_index n mod nat_of_index m)"
 
-lemma div_index_code [code func]:
+lemma div_index_code [code]:
   "index_of_nat n div index_of_nat m = index_of_nat (n div m)"
   by simp
 
-lemma mod_index_code [code func]:
+lemma mod_index_code [code]:
   "index_of_nat n mod index_of_nat m = index_of_nat (n mod m)"
   by simp
 
-definition [simp, code func del]:
+definition [simp, code del]:
   "n \<le> m \<longleftrightarrow> nat_of_index n \<le> nat_of_index m"
 
-definition [simp, code func del]:
+definition [simp, code del]:
   "n < m \<longleftrightarrow> nat_of_index n < nat_of_index m"
 
-lemma less_eq_index_code [code func]:
+lemma less_eq_index_code [code]:
   "index_of_nat n \<le> index_of_nat m \<longleftrightarrow> n \<le> m"
   by simp
 
-lemma less_index_code [code func]:
+lemma less_index_code [code]:
   "index_of_nat n < index_of_nat m \<longleftrightarrow> n < m"
   by simp
 
@@ -260,25 +260,25 @@
 definition
   minus_index_aux :: "index \<Rightarrow> index \<Rightarrow> index"
 where
-  [code func del]: "minus_index_aux = op -"
+  [code del]: "minus_index_aux = op -"
 
-lemma [code func]: "op - = minus_index_aux"
+lemma [code]: "op - = minus_index_aux"
   using minus_index_aux_def ..
 
 definition
   div_mod_index ::  "index \<Rightarrow> index \<Rightarrow> index \<times> index"
 where
-  [code func del]: "div_mod_index n m = (n div m, n mod m)"
+  [code del]: "div_mod_index n m = (n div m, n mod m)"
 
-lemma [code func]:
+lemma [code]:
   "div_mod_index n m = (if m = 0 then (0, n) else (n div m, n mod m))"
   unfolding div_mod_index_def by auto
 
-lemma [code func]:
+lemma [code]:
   "n div m = fst (div_mod_index n m)"
   unfolding div_mod_index_def by simp
 
-lemma [code func]:
+lemma [code]:
   "n mod m = snd (div_mod_index n m)"
   unfolding div_mod_index_def by simp
 
@@ -340,7 +340,7 @@
 
 text {* Evaluation *}
 
-lemma [code func, code func del]:
+lemma [code, code del]:
   "(Code_Eval.term_of \<Colon> index \<Rightarrow> term) = Code_Eval.term_of" ..
 
 code_const "Code_Eval.term_of \<Colon> index \<Rightarrow> term"
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Code_Integer.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -92,7 +92,7 @@
 
 text {* Evaluation *}
 
-lemma [code func, code func del]:
+lemma [code, code del]:
   "(Code_Eval.term_of \<Colon> int \<Rightarrow> term) = Code_Eval.term_of" ..
 
 code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term"
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Code_Message.thy
--- a/src/HOL/Library/Code_Message.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Code_Message.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -12,12 +12,12 @@
 
 datatype message_string = STR string
 
-lemmas [code func del] = message_string.recs message_string.cases
+lemmas [code del] = message_string.recs message_string.cases
 
-lemma [code func]: "size (s\<Colon>message_string) = 0"
+lemma [code]: "size (s\<Colon>message_string) = 0"
   by (cases s) simp_all
 
-lemma [code func]: "message_string_size (s\<Colon>message_string) = 0"
+lemma [code]: "message_string_size (s\<Colon>message_string) = 0"
   by (cases s) simp_all
 
 subsection {* ML interface *}
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -232,7 +232,6 @@
    of NONE => NONE
     | SOME thms4 => if Thm.eq_thms (map fst eqns2, thms4)
         then NONE else SOME (map (apfst (AxClass.overload thy) o Code_Unit.mk_eqn thy) thms4)
-          (*FIXME*)
   end
 
 in
@@ -344,13 +343,13 @@
 definition
   int :: "nat \<Rightarrow> int"
 where
-  [code func del]: "int = of_nat"
+  [code del]: "int = of_nat"
 
-lemma int_code' [code func]:
+lemma int_code' [code]:
   "int (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
   unfolding int_nat_number_of [folded int_def] ..
 
-lemma nat_code' [code func]:
+lemma nat_code' [code]:
   "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
   by auto
 
@@ -434,7 +433,7 @@
 
 text {* Evaluation *}
 
-lemma [code func, code func del]:
+lemma [code, code del]:
   "(Code_Eval.term_of \<Colon> nat \<Rightarrow> term) = Code_Eval.term_of" ..
 
 code_const "Code_Eval.term_of \<Colon> nat \<Rightarrow> term"
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Enum.thy
--- a/src/HOL/Library/Enum.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Enum.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -13,7 +13,7 @@
 
 class enum = itself +
   fixes enum :: "'a list"
-  assumes UNIV_enum [code func]: "UNIV = set enum"
+  assumes UNIV_enum [code]: "UNIV = set enum"
     and enum_distinct: "distinct enum"
 begin
 
@@ -49,7 +49,7 @@
 
 end
 
-lemma order_fun [code func]:
+lemma order_fun [code]:
   fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
   shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
     and "f < g \<longleftrightarrow> f \<le> g \<and> \<not> list_all (\<lambda>x. f x = g x) enum"
@@ -58,10 +58,10 @@
 
 subsection {* Quantifiers *}
 
-lemma all_code [code func]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
+lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
   by (simp add: list_all_iff enum_all)
 
-lemma exists_code [code func]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
+lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> \<not> list_all (Not o P) enum"
   by (simp add: list_all_iff enum_all)
 
 
@@ -157,7 +157,7 @@
 begin
 
 definition
-  [code func del]: "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
+  [code del]: "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
 
 instance proof
   show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
@@ -177,7 +177,7 @@
 
 end
 
-lemma enum_fun_code [code func]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
+lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, eq} list)
   in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
   by (simp add: enum_fun_def Let_def)
 
@@ -286,9 +286,9 @@
 begin
 
 definition
-  [code func del]: "enum = map (split Char) (product enum enum)"
+  [code del]: "enum = map (split Char) (product enum enum)"
 
-lemma enum_char [code func]:
+lemma enum_char [code]:
   "enum = [Char Nibble0 Nibble0, Char Nibble0 Nibble1, Char Nibble0 Nibble2,
   Char Nibble0 Nibble3, Char Nibble0 Nibble4, Char Nibble0 Nibble5,
   Char Nibble0 Nibble6, Char Nibble0 Nibble7, Char Nibble0 Nibble8,
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/GCD.thy
--- a/src/HOL/Library/GCD.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/GCD.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -18,7 +18,7 @@
 
 definition
   is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
-  [code func del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
+  [code del]: "is_gcd m n p \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
     (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
 
 text {* Uniqueness *}
@@ -776,7 +776,7 @@
   thus ?thesis by (simp add: zlcm_def)
 qed
 
-lemma zgcd_code [code func]:
+lemma zgcd_code [code]:
   "zgcd k l = \<bar>if l = 0 then k else zgcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
   by (simp add: zgcd_def gcd.simps [of "nat \<bar>k\<bar>"] nat_mod_distrib)
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Heap_Monad.thy
--- a/src/HOL/Library/Heap_Monad.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Heap_Monad.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -266,14 +266,14 @@
 definition
   Fail :: "message_string \<Rightarrow> exception"
 where
-  [code func del]: "Fail s = Exn"
+  [code del]: "Fail s = Exn"
 
 definition
   raise_exc :: "exception \<Rightarrow> 'a Heap"
 where
-  [code func del]: "raise_exc e = raise []"
+  [code del]: "raise_exc e = raise []"
 
-lemma raise_raise_exc [code func, code inline]:
+lemma raise_raise_exc [code, code inline]:
   "raise s = raise_exc (Fail (STR s))"
   unfolding Fail_def raise_exc_def raise_def ..
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/List_Prefix.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -15,10 +15,10 @@
 begin
 
 definition
-  prefix_def [code func del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"
+  prefix_def [code del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"
 
 definition
-  strict_prefix_def [code func del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"
+  strict_prefix_def [code del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"
 
 instance
   by intro_classes (auto simp add: prefix_def strict_prefix_def)
@@ -374,18 +374,18 @@
 
 subsection {* Executable code *}
 
-lemma less_eq_code [code func]:
+lemma less_eq_code [code]:
     "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
     "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
     "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
   by simp_all
 
-lemma less_code [code func]:
+lemma less_code [code]:
     "xs < ([]\<Colon>'a\<Colon>{eq, ord} list) \<longleftrightarrow> False"
     "[] < (x\<Colon>'a\<Colon>{eq, ord})# xs \<longleftrightarrow> True"
     "(x\<Colon>'a\<Colon>{eq, ord}) # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
   unfolding strict_prefix_def by auto
 
-lemmas [code func] = postfix_to_prefix
+lemmas [code] = postfix_to_prefix
 
 end
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/List_lexord.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -13,10 +13,10 @@
 begin
 
 definition
-  list_less_def [code func del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
+  list_less_def [code del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
 
 definition
-  list_le_def [code func del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
+  list_le_def [code del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
 
 instance ..
 
@@ -63,10 +63,10 @@
 begin
 
 definition
-  [code func del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
+  [code del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
 
 definition
-  [code func del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
+  [code del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
 
 instance
   by intro_classes
@@ -92,13 +92,13 @@
 lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
   by (unfold list_le_def) auto
 
-lemma less_code [code func]:
+lemma less_code [code]:
   "xs < ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
   "[] < (x\<Colon>'a\<Colon>{eq, order}) # xs \<longleftrightarrow> True"
   "(x\<Colon>'a\<Colon>{eq, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
   by simp_all
 
-lemma less_eq_code [code func]:
+lemma less_eq_code [code]:
   "x # xs \<le> ([]\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> False"
   "[] \<le> (xs\<Colon>'a\<Colon>{eq, order} list) \<longleftrightarrow> True"
   "(x\<Colon>'a\<Colon>{eq, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -29,7 +29,7 @@
   "single a = Abs_multiset (\<lambda>b. if b = a then 1 else 0)"
 
 declare
-  Mempty_def[code func del] single_def[code func del]
+  Mempty_def[code del] single_def[code del]
 
 definition
   count :: "'a multiset => 'a => nat" where
@@ -59,7 +59,7 @@
 begin
 
 definition
-  union_def[code func del]:
+  union_def[code del]:
   "M + N = Abs_multiset (\<lambda>a. Rep_multiset M a + Rep_multiset N a)"
 
 definition
@@ -69,7 +69,7 @@
   Zero_multiset_def [simp]: "0 = {#}"
 
 definition
-  size_def[code func del]: "size M = setsum (count M) (set_of M)"
+  size_def[code del]: "size M = setsum (count M) (set_of M)"
 
 instance ..
 
@@ -207,10 +207,10 @@
 
 subsubsection {* Size *}
 
-lemma size_empty [simp,code func]: "size {#} = 0"
+lemma size_empty [simp,code]: "size {#} = 0"
 by (simp add: size_def)
 
-lemma size_single [simp,code func]: "size {#b#} = 1"
+lemma size_single [simp,code]: "size {#b#} = 1"
 by (simp add: size_def)
 
 lemma finite_set_of [iff]: "finite (set_of M)"
@@ -223,7 +223,7 @@
 apply (simp add: Int_insert_left set_of_def)
 done
 
-lemma size_union[simp,code func]: "size (M + N::'a multiset) = size M + size N"
+lemma size_union[simp,code]: "size (M + N::'a multiset) = size M + size N"
 apply (unfold size_def)
 apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
  prefer 2
@@ -376,16 +376,16 @@
 
 subsubsection {* Comprehension (filter) *}
 
-lemma MCollect_empty[simp, code func]: "MCollect {#} P = {#}"
+lemma MCollect_empty[simp, code]: "MCollect {#} P = {#}"
 by (simp add: MCollect_def Mempty_def Abs_multiset_inject
     in_multiset expand_fun_eq)
 
-lemma MCollect_single[simp, code func]:
+lemma MCollect_single[simp, code]:
   "MCollect {#x#} P = (if P x then {#x#} else {#})"
 by (simp add: MCollect_def Mempty_def single_def Abs_multiset_inject
     in_multiset expand_fun_eq)
 
-lemma MCollect_union[simp, code func]:
+lemma MCollect_union[simp, code]:
   "MCollect (M+N) f = MCollect M f + MCollect N f"
 by (simp add: MCollect_def union_def Abs_multiset_inject
     in_multiset expand_fun_eq)
@@ -500,7 +500,7 @@
 
 definition
   mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
-  [code func del]:"mult1 r =
+  [code del]:"mult1 r =
     {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
       (\<forall>b. b :# K --> (b, a) \<in> r)}"
 
@@ -716,10 +716,10 @@
 begin
 
 definition
-  less_multiset_def [code func del]: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
+  less_multiset_def [code del]: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
 
 definition
-  le_multiset_def [code func del]: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
+  le_multiset_def [code del]: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
 
 lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
 unfolding trans_def by (blast intro: order_less_trans)
@@ -983,11 +983,11 @@
 
 definition
   mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<le>#" 50) where
-  [code func del]: "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
+  [code del]: "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
 
 definition
   mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "<#" 50) where
-  [code func del]: "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
+  [code del]: "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
 
 notation mset_le  (infix "\<subseteq>#" 50)
 notation mset_less  (infix "\<subset>#" 50)
@@ -1448,22 +1448,22 @@
 
 subsection {* Image *}
 
-definition [code func del]: "image_mset f == fold_mset (op + o single o f) {#}"
+definition [code del]: "image_mset f == fold_mset (op + o single o f) {#}"
 
 interpretation image_left_comm: left_commutative ["op + o single o f"]
 by (unfold_locales) (simp add:union_ac)
 
-lemma image_mset_empty [simp, code func]: "image_mset f {#} = {#}"
+lemma image_mset_empty [simp, code]: "image_mset f {#} = {#}"
 by (simp add: image_mset_def)
 
-lemma image_mset_single [simp, code func]: "image_mset f {#x#} = {#f x#}"
+lemma image_mset_single [simp, code]: "image_mset f {#x#} = {#f x#}"
 by (simp add: image_mset_def)
 
 lemma image_mset_insert:
   "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
 by (simp add: image_mset_def add_ac)
 
-lemma image_mset_union[simp, code func]:
+lemma image_mset_union[simp, code]:
   "image_mset f (M+N) = image_mset f M + image_mset f N"
 apply (induct N)
  apply simp
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -37,7 +37,7 @@
   [code inline]: "1 = Fin 1"
 
 definition
-  [code inline, code func del]: "number_of k = Fin (number_of k)"
+  [code inline, code del]: "number_of k = Fin (number_of k)"
 
 instance ..
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Nested_Environment.thy
--- a/src/HOL/Library/Nested_Environment.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Nested_Environment.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -525,11 +525,11 @@
 
 text {* Environments and code generation *}
 
-lemma [code func, code func del]:
+lemma [code, code del]:
   fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
   shows "eq_class.eq e1 e2 \<longleftrightarrow> eq_class.eq e1 e2" ..
 
-lemma eq_env_code [code func]:
+lemma eq_env_code [code]:
   fixes x y :: "'a\<Colon>eq"
     and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option"
   shows "eq_class.eq (Env x f) (Env y g) \<longleftrightarrow>
@@ -567,7 +567,7 @@
           of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
 qed simp_all
 
-lemma [code func, code func del]:
+lemma [code, code del]:
   "(Code_Eval.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Eval.term_of" ..
 
 end
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Option_ord.thy
--- a/src/HOL/Library/Option_ord.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Option_ord.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -13,10 +13,10 @@
 begin
 
 definition less_eq_option where
-  [code func del]: "x \<le> y \<longleftrightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> x \<le> y))"
+  [code del]: "x \<le> y \<longleftrightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> x \<le> y))"
 
 definition less_option where
-  [code func del]: "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> x < y))"
+  [code del]: "x < y \<longleftrightarrow> (case y of None \<Rightarrow> False | Some y \<Rightarrow> (case x of None \<Rightarrow> True | Some x \<Rightarrow> x < y))"
 
 lemma less_eq_option_None [simp]: "None \<le> x"
   by (simp add: less_eq_option_def)
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Primes.thy
--- a/src/HOL/Library/Primes.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Primes.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -16,7 +16,7 @@
 
 definition
   prime :: "nat \<Rightarrow> bool" where
-  [code func del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
+  [code del]: "prime p \<longleftrightarrow> (1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p))"
 
 
 lemma two_is_prime: "prime 2"
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Product_ord.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -13,16 +13,16 @@
 begin
 
 definition
-  prod_le_def [code func del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
+  prod_le_def [code del]: "x \<le> y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x \<le> snd y"
 
 definition
-  prod_less_def [code func del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
+  prod_less_def [code del]: "x < y \<longleftrightarrow> fst x < fst y \<or> fst x = fst y \<and> snd x < snd y"
 
 instance ..
 
 end
 
-lemma [code func]:
+lemma [code]:
   "(x1\<Colon>'a\<Colon>{ord, eq}, y1) \<le> (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 \<le> y2"
   "(x1\<Colon>'a\<Colon>{ord, eq}, y1) < (x2, y2) \<longleftrightarrow> x1 < x2 \<or> x1 = x2 \<and> y1 < y2"
   unfolding prod_le_def prod_less_def by simp_all
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/RType.thy
--- a/src/HOL/Library/RType.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/RType.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -89,7 +89,7 @@
   #> TypedefPackage.interpretation Typerep.perhaps_add_def
 *}
 
-lemma [code func]:
+lemma [code]:
   "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
      \<and> list_all2 eq_class.eq tys1 tys2"
   by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Ref.thy
--- a/src/HOL/Library/Ref.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Ref.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -51,7 +51,7 @@
   by (cases f)
     (auto simp add: Let_def bindM_def lookup_def expand_fun_eq)
 
-lemma update_change [code func]:
+lemma update_change [code]:
   "r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()"
   by (auto simp add: monad_simp change_def lookup_chain)
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Sublist_Order.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -47,7 +47,7 @@
   using assms by (induct rule: less_eq_list.induct) blast+
 
 definition
-  [code func del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
+  [code del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
 
 lemma ileq_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
   by (induct rule: ileq_induct) auto
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Univ_Poly.thy
--- a/src/HOL/Library/Univ_Poly.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Univ_Poly.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -72,7 +72,7 @@
 
 definition (in semiring_0)
   divides :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "divides" 70) where
-  [code func del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
+  [code del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
 
     --{*order of a polynomial*}
 definition (in ring_1) order :: "'a => 'a list => nat" where
diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Word.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -2042,7 +2042,7 @@
 
 definition
   length_nat :: "nat => nat" where
-  [code func del]: "length_nat x = (LEAST n. x < 2 ^ n)"
+  [code del]: "length_nat x = (LEAST n. x < 2 ^ n)"
 
 lemma length_nat: "length (nat_to_bv n) = length_nat n"
   apply (simp add: length_nat_def)
@@ -2267,7 +2267,7 @@
   fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k =
     fast_bv_to_nat_helper bs ((bit_case Int.Bit0 Int.Bit1 b) k)"
 
-declare fast_bv_to_nat_helper.simps [code func del]
+declare fast_bv_to_nat_helper.simps [code del]
 
 lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin =
     fast_bv_to_nat_helper bs (Int.Bit0 bin)"
diff -r 056255ade52a -r 4e74209f113e src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/List.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -204,7 +204,7 @@
 
 definition
   list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
-  [code func del]: "list_all2 P xs ys =
+  [code del]: "list_all2 P xs ys =
     (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
 
 definition
@@ -2872,7 +2872,7 @@
 
 definition
  sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
- [code func del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
+ [code del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
 
 lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
   set(sorted_list_of_set A) = A &
@@ -3057,7 +3057,7 @@
 constdefs
   set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
   "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
-declare set_Cons_def [code func del]
+declare set_Cons_def [code del]
 
 lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
 by (auto simp add: set_Cons_def)
@@ -3095,7 +3095,7 @@
     "lenlex r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
         --{*Compares lists by their length and then lexicographically*}
 
-declare lex_def [code func del]
+declare lex_def [code del]
 
 
 lemma wf_lexn: "wf r ==> wf (lexn r n)"
@@ -3171,7 +3171,7 @@
   lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set" 
   "lexord  r == {(x,y). \<exists> a v. y = x @ a # v \<or> 
             (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
-declare lexord_def [code func del]
+declare lexord_def [code del]
 
 lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
 by (unfold lexord_def, induct_tac y, auto) 
@@ -3379,7 +3379,7 @@
 primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
   "nibble_pair_of_char (Char n m) = (n, m)"
 
-declare nibble_pair_of_char.simps [code func del]
+declare nibble_pair_of_char.simps [code del]
 
 setup {*
 let
@@ -3393,11 +3393,11 @@
 end
 *}
 
-lemma char_case_nibble_pair [code func, code inline]:
+lemma char_case_nibble_pair [code, code inline]:
   "char_case f = split f o nibble_pair_of_char"
   by (simp add: expand_fun_eq split: char.split)
 
-lemma char_rec_nibble_pair [code func, code inline]:
+lemma char_rec_nibble_pair [code, code inline]:
   "char_rec f = split f o nibble_pair_of_char"
   unfolding char_case_nibble_pair [symmetric]
   by (simp add: expand_fun_eq split: char.split)
diff -r 056255ade52a -r 4e74209f113e src/HOL/Map.thy
--- a/src/HOL/Map.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Map.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -91,7 +91,7 @@
   by simp_all
 
 defs
-  map_upds_def [code func]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
+  map_upds_def [code]: "m(xs [|->] ys) == m ++ map_of (rev(zip xs ys))"
 
 
 subsection {* @{term [source] empty} *}
diff -r 056255ade52a -r 4e74209f113e src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -768,7 +768,7 @@
 instantiation matrix :: (zero) zero
 begin
 
-definition zero_matrix_def [code func del]: "0 = Abs_matrix (\<lambda>j i. 0)"
+definition zero_matrix_def [code del]: "0 = Abs_matrix (\<lambda>j i. 0)"
 
 instance ..
 
@@ -1440,9 +1440,9 @@
 instantiation matrix :: ("{lattice, zero}") lattice
 begin
 
-definition [code func del]: "inf = combine_matrix inf"
+definition [code del]: "inf = combine_matrix inf"
 
-definition [code func del]: "sup = combine_matrix sup"
+definition [code del]: "sup = combine_matrix sup"
 
 instance
   by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
@@ -1453,7 +1453,7 @@
 begin
 
 definition
-  plus_matrix_def [code func del]: "A + B = combine_matrix (op +) A B"
+  plus_matrix_def [code del]: "A + B = combine_matrix (op +) A B"
 
 instance ..
 
@@ -1463,7 +1463,7 @@
 begin
 
 definition
-  minus_matrix_def [code func del]: "- A = apply_matrix uminus A"
+  minus_matrix_def [code del]: "- A = apply_matrix uminus A"
 
 instance ..
 
@@ -1473,7 +1473,7 @@
 begin
 
 definition
-  diff_matrix_def [code func del]: "A - B = combine_matrix (op -) A B"
+  diff_matrix_def [code del]: "A - B = combine_matrix (op -) A B"
 
 instance ..
 
@@ -1483,7 +1483,7 @@
 begin
 
 definition
-  times_matrix_def [code func del]: "A * B = mult_matrix (op *) (op +) A B"
+  times_matrix_def [code del]: "A * B = mult_matrix (op *) (op +) A B"
 
 instance ..
 
@@ -1493,7 +1493,7 @@
 begin
 
 definition
-  abs_matrix_def [code func del]: "abs (A \<Colon> 'a matrix) = sup A (- A)"
+  abs_matrix_def [code del]: "abs (A \<Colon> 'a matrix) = sup A (- A)"
 
 instance ..
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/Matrix/SparseMatrix.thy
--- a/src/HOL/Matrix/SparseMatrix.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -25,7 +25,7 @@
 lemma sparse_row_matrix_empty [simp]: "sparse_row_matrix [] = 0"
   by (simp add: sparse_row_matrix_def)
 
-lemmas [code func] = sparse_row_vector_empty [symmetric]
+lemmas [code] = sparse_row_vector_empty [symmetric]
 
 lemma foldl_distrstart[rule_format]: "! a x y. (f (g x y) a = g x (f y a)) \<Longrightarrow> ! x y. (foldl f (g x y) l = g x (foldl f y l))"
   by (induct l, auto)
@@ -417,8 +417,8 @@
   apply (auto simp add: sparse_row_matrix_cons sparse_row_vector_add move_matrix_add)
   done
 
-lemmas [code func] = sparse_row_add_spmat [symmetric]
-lemmas [code func] = sparse_row_vector_add [symmetric]
+lemmas [code] = sparse_row_add_spmat [symmetric]
+lemmas [code] = sparse_row_vector_add [symmetric]
 
 lemma sorted_add_spvec_helper1[rule_format]: "add_spvec ((a,b)#arr, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))"
   proof - 
diff -r 056255ade52a -r 4e74209f113e src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -68,7 +68,7 @@
 definition
   "wf_class G = wfP ((subcls1 G)^--1)"
 
-lemma class_rec_func (*[code func]*):
+lemma class_rec_func (*[code]*):
   "class_rec G C t f = (if wf_class G then
     (case class G C
       of None \<Rightarrow> undefined
diff -r 056255ade52a -r 4e74209f113e src/HOL/NSA/HDeriv.thy
--- a/src/HOL/NSA/HDeriv.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/HDeriv.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -27,7 +27,7 @@
 
 definition
   increment :: "[real=>real,real,hypreal] => hypreal" where
-  [code func del]: "increment f x h = (@inc. f NSdifferentiable x &
+  [code del]: "increment f x h = (@inc. f NSdifferentiable x &
            inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))"
 
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/NSA/HLim.thy
--- a/src/HOL/NSA/HLim.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/HLim.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -16,18 +16,18 @@
 definition
   NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
             ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
-  [code func del]: "f -- a --NS> L =
+  [code del]: "f -- a --NS> L =
     (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
 
 definition
   isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
     --{*NS definition dispenses with limit notions*}
-  [code func del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
+  [code del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
          ( *f* f) y @= star_of (f a))"
 
 definition
   isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
-  [code func del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
+  [code del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
 
 
 subsection {* Limits of Functions *}
diff -r 056255ade52a -r 4e74209f113e src/HOL/NSA/HLog.thy
--- a/src/HOL/NSA/HLog.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/HLog.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -20,11 +20,11 @@
 
 definition
   powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80) where
-  [transfer_unfold, code func del]: "x powhr a = starfun2 (op powr) x a"
+  [transfer_unfold, code del]: "x powhr a = starfun2 (op powr) x a"
   
 definition
   hlog :: "[hypreal,hypreal] => hypreal" where
-  [transfer_unfold, code func del]: "hlog a x = starfun2 log a x"
+  [transfer_unfold, code del]: "hlog a x = starfun2 log a x"
 
 lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
 by (simp add: powhr_def starfun2_star_n)
diff -r 056255ade52a -r 4e74209f113e src/HOL/NSA/HSEQ.thy
--- a/src/HOL/NSA/HSEQ.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/HSEQ.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -16,7 +16,7 @@
   NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
     ("((_)/ ----NS> (_))" [60, 60] 60) where
     --{*Nonstandard definition of convergence of sequence*}
-  [code func del]: "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
+  [code del]: "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
 
 definition
   nslim :: "(nat => 'a::real_normed_vector) => 'a" where
@@ -31,12 +31,12 @@
 definition
   NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
     --{*Nonstandard definition for bounded sequence*}
-  [code func del]: "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
+  [code del]: "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
 
 definition
   NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
     --{*Nonstandard definition*}
-  [code func del]: "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
+  [code del]: "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
 
 subsection {* Limits of Sequences *}
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/NSA/HSeries.thy
--- a/src/HOL/NSA/HSeries.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/HSeries.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -13,7 +13,7 @@
 
 definition
   sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where
-  [code func del]: "sumhr = 
+  [code del]: "sumhr = 
       (%(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N)"
 
 definition
@@ -22,7 +22,7 @@
 
 definition
   NSsummable :: "(nat=>real) => bool" where
-  [code func del]: "NSsummable f = (\<exists>s. f NSsums s)"
+  [code del]: "NSsummable f = (\<exists>s. f NSsums s)"
 
 definition
   NSsuminf   :: "(nat=>real) => real" where
diff -r 056255ade52a -r 4e74209f113e src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -47,7 +47,7 @@
 begin
 
 definition
-  star_scaleR_def [transfer_unfold, code func del]: "scaleR r \<equiv> *f* (scaleR r)"
+  star_scaleR_def [transfer_unfold, code del]: "scaleR r \<equiv> *f* (scaleR r)"
 
 instance ..
 
@@ -113,7 +113,7 @@
 
 definition
   of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where
-  [transfer_unfold, code func del]: "of_hypreal = *f* of_real"
+  [transfer_unfold, code del]: "of_hypreal = *f* of_real"
 
 lemma Standard_of_hypreal [simp]:
   "r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard"
@@ -428,7 +428,7 @@
 subsection{*Powers with Hypernatural Exponents*}
 
 definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
-  hyperpow_def [transfer_unfold, code func del]: "R pow N = ( *f2* op ^) R N"
+  hyperpow_def [transfer_unfold, code del]: "R pow N = ( *f2* op ^) R N"
   (* hypernatural powers of hyperreals *)
 
 lemma Standard_hyperpow [simp]:
diff -r 056255ade52a -r 4e74209f113e src/HOL/NSA/HyperNat.thy
--- a/src/HOL/NSA/HyperNat.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/HyperNat.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -19,7 +19,7 @@
 
 definition
   hSuc :: "hypnat => hypnat" where
-  hSuc_def [transfer_unfold, code func del]: "hSuc = *f* Suc"
+  hSuc_def [transfer_unfold, code del]: "hSuc = *f* Suc"
 
 subsection{*Properties Transferred from Naturals*}
 
@@ -367,7 +367,7 @@
 
 definition
   of_hypnat :: "hypnat \<Rightarrow> 'a::semiring_1_cancel star" where
-  of_hypnat_def [transfer_unfold, code func del]: "of_hypnat = *f* of_nat"
+  of_hypnat_def [transfer_unfold, code del]: "of_hypnat = *f* of_nat"
 
 lemma of_hypnat_0 [simp]: "of_hypnat 0 = 0"
 by transfer (rule of_nat_0)
diff -r 056255ade52a -r 4e74209f113e src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/NSA.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -17,15 +17,15 @@
 
 definition
   Infinitesimal  :: "('a::real_normed_vector) star set" where
-  [code func del]: "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
+  [code del]: "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
 
 definition
   HFinite :: "('a::real_normed_vector) star set" where
-  [code func del]: "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
+  [code del]: "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
 
 definition
   HInfinite :: "('a::real_normed_vector) star set" where
-  [code func del]: "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
+  [code del]: "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
 
 definition
   approx :: "['a::real_normed_vector star, 'a star] => bool"  (infixl "@=" 50) where
@@ -58,7 +58,7 @@
 
 definition
   scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where
-  [transfer_unfold, code func del]: "scaleHR = starfun2 scaleR"
+  [transfer_unfold, code del]: "scaleHR = starfun2 scaleR"
 
 lemma Standard_hnorm [simp]: "x \<in> Standard \<Longrightarrow> hnorm x \<in> Standard"
 by (simp add: hnorm_def)
diff -r 056255ade52a -r 4e74209f113e src/HOL/NSA/NSCA.thy
--- a/src/HOL/NSA/NSCA.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/NSCA.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -16,7 +16,7 @@
 
 definition --{* standard part map*}
   stc :: "hcomplex => hcomplex" where 
-  [code func del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
+  [code del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
 
 
 subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
diff -r 056255ade52a -r 4e74209f113e src/HOL/NSA/NSComplex.thy
--- a/src/HOL/NSA/NSComplex.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/NSComplex.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -26,11 +26,11 @@
 
 definition
   hRe :: "hcomplex => hypreal" where
-  [code func del]: "hRe = *f* Re"
+  [code del]: "hRe = *f* Re"
 
 definition
   hIm :: "hcomplex => hypreal" where
-  [code func del]: "hIm = *f* Im"
+  [code del]: "hIm = *f* Im"
 
 
   (*------ imaginary unit ----------*)
@@ -43,22 +43,22 @@
 
 definition
   hcnj :: "hcomplex => hcomplex" where
-  [code func del]: "hcnj = *f* cnj"
+  [code del]: "hcnj = *f* cnj"
 
   (*------------ Argand -------------*)
 
 definition
   hsgn :: "hcomplex => hcomplex" where
-  [code func del]: "hsgn = *f* sgn"
+  [code del]: "hsgn = *f* sgn"
 
 definition
   harg :: "hcomplex => hypreal" where
-  [code func del]: "harg = *f* arg"
+  [code del]: "harg = *f* arg"
 
 definition
   (* abbreviation for (cos a + i sin a) *)
   hcis :: "hypreal => hcomplex" where
-  [code func del]:"hcis = *f* cis"
+  [code del]:"hcis = *f* cis"
 
   (*----- injection from hyperreals -----*)
 
@@ -69,16 +69,16 @@
 definition
   (* abbreviation for r*(cos a + i sin a) *)
   hrcis :: "[hypreal, hypreal] => hcomplex" where
-  [code func del]: "hrcis = *f2* rcis"
+  [code del]: "hrcis = *f2* rcis"
 
   (*------------ e ^ (x + iy) ------------*)
 definition
   hexpi :: "hcomplex => hcomplex" where
-  [code func del]: "hexpi = *f* expi"
+  [code del]: "hexpi = *f* expi"
 
 definition
   HComplex :: "[hypreal,hypreal] => hcomplex" where
-  [code func del]: "HComplex = *f2* Complex"
+  [code del]: "HComplex = *f2* Complex"
 
 lemmas hcomplex_defs [transfer_unfold] =
   hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
diff -r 056255ade52a -r 4e74209f113e src/HOL/NSA/Star.thy
--- a/src/HOL/NSA/Star.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/Star.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -17,12 +17,12 @@
 
 definition
   InternalSets :: "'a star set set" where
-  [code func del]: "InternalSets = {X. \<exists>As. X = *sn* As}"
+  [code del]: "InternalSets = {X. \<exists>As. X = *sn* As}"
 
 definition
   (* nonstandard extension of function *)
   is_starext  :: "['a star => 'a star, 'a => 'a] => bool" where
-  [code func del]: "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
+  [code del]: "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
                         ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
 
 definition
@@ -32,7 +32,7 @@
 
 definition
   InternalFuns :: "('a star => 'b star) set" where
-  [code func del]:"InternalFuns = {X. \<exists>F. X = *fn* F}"
+  [code del]:"InternalFuns = {X. \<exists>F. X = *fn* F}"
 
 
 (*--------------------------------------------------------
diff -r 056255ade52a -r 4e74209f113e src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NSA/StarDef.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -291,7 +291,7 @@
 subsection {* Internal predicates *}
 
 definition unstar :: "bool star \<Rightarrow> bool" where
-  [code func del]: "unstar b \<longleftrightarrow> b = star_of True"
+  [code del]: "unstar b \<longleftrightarrow> b = star_of True"
 
 lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
 by (simp add: unstar_def star_of_def star_n_eq_iff)
@@ -432,7 +432,7 @@
 begin
 
 definition
-  star_zero_def [code func del]:    "0 \<equiv> star_of 0"
+  star_zero_def [code del]:    "0 \<equiv> star_of 0"
 
 instance ..
 
@@ -442,7 +442,7 @@
 begin
 
 definition
-  star_one_def [code func del]:     "1 \<equiv> star_of 1"
+  star_one_def [code del]:     "1 \<equiv> star_of 1"
 
 instance ..
 
@@ -452,7 +452,7 @@
 begin
 
 definition
-  star_add_def [code func del]:     "(op +) \<equiv> *f2* (op +)"
+  star_add_def [code del]:     "(op +) \<equiv> *f2* (op +)"
 
 instance ..
 
@@ -462,7 +462,7 @@
 begin
 
 definition
-  star_mult_def [code func del]:    "(op *) \<equiv> *f2* (op *)"
+  star_mult_def [code del]:    "(op *) \<equiv> *f2* (op *)"
 
 instance ..
 
@@ -472,7 +472,7 @@
 begin
 
 definition
-  star_minus_def [code func del]:   "uminus \<equiv> *f* uminus"
+  star_minus_def [code del]:   "uminus \<equiv> *f* uminus"
 
 instance ..
 
@@ -482,7 +482,7 @@
 begin
 
 definition
-  star_diff_def [code func del]:    "(op -) \<equiv> *f2* (op -)"
+  star_diff_def [code del]:    "(op -) \<equiv> *f2* (op -)"
 
 instance ..
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Nat.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -55,7 +55,7 @@
 instantiation nat :: zero
 begin
 
-definition Zero_nat_def [code func del]:
+definition Zero_nat_def [code del]:
   "0 = Abs_Nat Zero_Rep"
 
 instance ..
@@ -1281,7 +1281,7 @@
 
 definition
   Nats  :: "'a set" where
-  [code func del]: "Nats = range of_nat"
+  [code del]: "Nats = range of_nat"
 
 notation (xsymbols)
   Nats  ("\<nat>")
diff -r 056255ade52a -r 4e74209f113e src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/NatBin.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -18,7 +18,7 @@
 begin
 
 definition
-  nat_number_of_def [code inline, code func del]: "number_of v = nat (number_of v)"
+  nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
 
 instance ..
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Orderings.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -968,10 +968,10 @@
 begin
 
 definition
-  le_bool_def [code func del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
+  le_bool_def [code del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
 
 definition
-  less_bool_def [code func del]: "(P\<Colon>bool) < Q \<longleftrightarrow> P \<le> Q \<and> P \<noteq> Q"
+  less_bool_def [code del]: "(P\<Colon>bool) < Q \<longleftrightarrow> P \<le> Q \<and> P \<noteq> Q"
 
 instance
   by intro_classes (auto simp add: le_bool_def less_bool_def)
@@ -990,7 +990,7 @@
 lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
 by (simp add: le_bool_def)
 
-lemma [code func]:
+lemma [code]:
   "False \<le> b \<longleftrightarrow> True"
   "True \<le> b \<longleftrightarrow> b"
   "False < b \<longleftrightarrow> b"
@@ -1004,10 +1004,10 @@
 begin
 
 definition
-  le_fun_def [code func del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
+  le_fun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
 
 definition
-  less_fun_def [code func del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> f \<noteq> g"
+  less_fun_def [code del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> f \<noteq> g"
 
 instance ..
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Product_Type.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -23,10 +23,10 @@
   -- "prefer plain propositional version"
 
 lemma
-  shows [code func]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
-    and [code func]: "eq_class.eq True P \<longleftrightarrow> P" 
-    and [code func]: "eq_class.eq P False \<longleftrightarrow> \<not> P" 
-    and [code func]: "eq_class.eq P True \<longleftrightarrow> P"
+  shows [code]: "eq_class.eq False P \<longleftrightarrow> \<not> P"
+    and [code]: "eq_class.eq True P \<longleftrightarrow> P" 
+    and [code]: "eq_class.eq P False \<longleftrightarrow> \<not> P" 
+    and [code]: "eq_class.eq P True \<longleftrightarrow> P"
     and [code nbe]: "eq_class.eq P P \<longleftrightarrow> True"
   by (simp_all add: eq)
 
@@ -89,7 +89,7 @@
 
 instance unit :: eq ..
 
-lemma [code func]:
+lemma [code]:
   "eq_class.eq (u\<Colon>unit) v \<longleftrightarrow> True" unfolding eq unit_eq [of u] unit_eq [of v] by rule+
 
 code_type unit
@@ -359,10 +359,10 @@
 
 subsubsection {* @{text split} and @{text curry} *}
 
-lemma split_conv [simp, code func]: "split f (a, b) = f a b"
+lemma split_conv [simp, code]: "split f (a, b) = f a b"
   by (simp add: split_def)
 
-lemma curry_conv [simp, code func]: "curry f a b = f (a, b)"
+lemma curry_conv [simp, code]: "curry f a b = f (a, b)"
   by (simp add: curry_def)
 
 lemmas split = split_conv  -- {* for backwards compatibility *}
@@ -728,9 +728,9 @@
 *}
 
 definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
-  [code func del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
+  [code del]: "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
 
-lemma prod_fun [simp, code func]: "prod_fun f g (a, b) = (f a, g b)"
+lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)"
   by (simp add: prod_fun_def)
 
 lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
@@ -758,12 +758,12 @@
 definition
   apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
 where
-  [code func del]: "apfst f = prod_fun f id"
+  [code del]: "apfst f = prod_fun f id"
 
 definition
   apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c"
 where
-  [code func del]: "apsnd f = prod_fun id f"
+  [code del]: "apsnd f = prod_fun id f"
 
 lemma apfst_conv [simp, code]:
   "apfst f (x, y) = (f x, y)" 
@@ -917,7 +917,7 @@
 
 instance * :: (eq, eq) eq ..
 
-lemma [code func]:
+lemma [code]:
   "eq_class.eq (x1\<Colon>'a\<Colon>eq, y1\<Colon>'b\<Colon>eq) (x2, y2) \<longleftrightarrow> x1 = x2 \<and> y1 = y2" by (simp add: eq)
 
 lemma split_case_cert:
diff -r 056255ade52a -r 4e74209f113e src/HOL/Real/ContNotDenum.thy
--- a/src/HOL/Real/ContNotDenum.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Real/ContNotDenum.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -403,7 +403,7 @@
        (f (Suc n)) \<notin> e)
       )"
 
-declare newInt.simps [code func del]
+declare newInt.simps [code del]
 
 subsubsection {* Properties *}
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Real/PReal.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -19,7 +19,7 @@
 
 definition
   cut :: "rat set => bool" where
-  [code func del]: "cut A = ({} \<subset> A &
+  [code del]: "cut A = ({} \<subset> A &
             A < {r. 0 < r} &
             (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
 
@@ -56,7 +56,7 @@
 
 definition
   diff_set :: "[rat set,rat set] => rat set" where
-  [code func del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
+  [code del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
 
 definition
   mult_set :: "[rat set,rat set] => rat set" where
@@ -64,17 +64,17 @@
 
 definition
   inverse_set :: "rat set => rat set" where
-  [code func del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
+  [code del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
 
 instantiation preal :: "{ord, plus, minus, times, inverse, one}"
 begin
 
 definition
-  preal_less_def [code func del]:
+  preal_less_def [code del]:
     "R < S == Rep_preal R < Rep_preal S"
 
 definition
-  preal_le_def [code func del]:
+  preal_le_def [code del]:
     "R \<le> S == Rep_preal R \<subseteq> Rep_preal S"
 
 definition
diff -r 056255ade52a -r 4e74209f113e src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Real/RComplete.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -488,7 +488,7 @@
 
 definition
   floor :: "real => int" where
-  [code func del]: "floor r = (LEAST n::int. r < real (n+1))"
+  [code del]: "floor r = (LEAST n::int. r < real (n+1))"
 
 definition
   ceiling :: "real => int" where
diff -r 056255ade52a -r 4e74209f113e src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Real/Rational.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -71,7 +71,7 @@
 
 definition
   Fract :: "int \<Rightarrow> int \<Rightarrow> rat" where
-  [code func del]: "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})"
+  [code del]: "Fract a b = Abs_Rat (ratrel `` {if b = 0 then (0, 1) else (a, b)})"
 
 code_datatype Fract
 
@@ -101,7 +101,7 @@
   One_rat_def [code, code unfold]: "1 = Fract 1 1"
 
 definition
-  add_rat_def [code func del]:
+  add_rat_def [code del]:
   "q + r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
     ratrel `` {(fst x * snd y + fst y * snd x, snd x * snd y)})"
 
@@ -116,7 +116,7 @@
 qed
 
 definition
-  minus_rat_def [code func del]:
+  minus_rat_def [code del]:
   "- q = Abs_Rat (\<Union>x \<in> Rep_Rat q. ratrel `` {(- fst x, snd x)})"
 
 lemma minus_rat [simp, code]: "- Fract a b = Fract (- a) b"
@@ -130,7 +130,7 @@
   by (cases "b = 0") (simp_all add: eq_rat)
 
 definition
-  diff_rat_def [code func del]: "q - r = q + - (r::rat)"
+  diff_rat_def [code del]: "q - r = q + - (r::rat)"
 
 lemma diff_rat [simp]:
   assumes "b \<noteq> 0" and "d \<noteq> 0"
@@ -138,7 +138,7 @@
   using assms by (simp add: diff_rat_def)
 
 definition
-  mult_rat_def [code func del]:
+  mult_rat_def [code del]:
   "q * r = Abs_Rat (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
     ratrel``{(fst x * fst y, snd x * snd y)})"
 
@@ -219,7 +219,7 @@
 begin
 
 definition
-  rat_number_of_def [code func del]: "number_of w = Fract w 1"
+  rat_number_of_def [code del]: "number_of w = Fract w 1"
 
 instance by intro_classes (simp add: rat_number_of_def of_int_rat)
 
@@ -265,7 +265,7 @@
 begin
 
 definition
-  inverse_rat_def [code func del]:
+  inverse_rat_def [code del]:
   "inverse q = Abs_Rat (\<Union>x \<in> Rep_Rat q.
      ratrel `` {if fst x = 0 then (0, 1) else (snd x, fst x)})"
 
@@ -277,7 +277,7 @@
 qed
 
 definition
-  divide_rat_def [code func del]: "q / r = q * inverse (r::rat)"
+  divide_rat_def [code del]: "q / r = q * inverse (r::rat)"
 
 lemma divide_rat [simp]: "Fract a b / Fract c d = Fract (a * d) (b * c)"
   by (simp add: divide_rat_def)
@@ -320,7 +320,7 @@
 begin
 
 definition
-  le_rat_def [code func del]:
+  le_rat_def [code del]:
    "q \<le> r \<longleftrightarrow> contents (\<Union>x \<in> Rep_Rat q. \<Union>y \<in> Rep_Rat r.
       {(fst x * snd y) * (snd x * snd y) \<le> (fst y * snd x) * (snd x * snd y)})"
 
@@ -370,7 +370,7 @@
 qed
 
 definition
-  less_rat_def [code func del]: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
+  less_rat_def [code del]: "z < (w::rat) \<longleftrightarrow> z \<le> w \<and> z \<noteq> w"
 
 lemma less_rat [simp]:
   assumes "b \<noteq> 0" and "d \<noteq> 0"
@@ -450,13 +450,13 @@
 begin
 
 definition
-  abs_rat_def [code func del]: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))"
+  abs_rat_def [code del]: "\<bar>q\<bar> = (if q < 0 then -q else (q::rat))"
 
 lemma abs_rat [simp, code]: "\<bar>Fract a b\<bar> = Fract \<bar>a\<bar> \<bar>b\<bar>"
   by (auto simp add: abs_rat_def zabs_def Zero_rat_def less_rat not_less le_less minus_rat eq_rat zero_compare_simps)
 
 definition
-  sgn_rat_def [code func del]: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)"
+  sgn_rat_def [code del]: "sgn (q::rat) = (if q = 0 then 0 else if 0 < q then 1 else - 1)"
 
 lemma sgn_rat [simp, code]: "sgn (Fract a b) = of_int (sgn a * sgn b)"
   unfolding Fract_of_int_eq
@@ -553,7 +553,7 @@
 begin
 
 definition of_rat :: "rat \<Rightarrow> 'a" where
-  [code func del]: "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
+  [code del]: "of_rat q = contents (\<Union>(a,b) \<in> Rep_Rat q. {of_int a / of_int b})"
 
 end
 
@@ -680,7 +680,7 @@
 
 definition
   Rats  :: "'a set" where
-  [code func del]: "Rats = range of_rat"
+  [code del]: "Rats = range of_rat"
 
 notation (xsymbols)
   Rats  ("\<rat>")
@@ -850,9 +850,9 @@
 qed
 
 definition Fract_norm :: "int \<Rightarrow> int \<Rightarrow> rat" where
-  [simp, code func del]: "Fract_norm a b = Fract a b"
+  [simp, code del]: "Fract_norm a b = Fract a b"
 
-lemma [code func]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in
+lemma [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in
   if b > 0 then Fract (a div c) (b div c) else Fract (- (a div c)) (- (b div c)))"
   by (simp add: eq_rat Zero_rat_def Let_def Fract_norm)
 
@@ -863,7 +863,7 @@
 instantiation rat :: eq
 begin
 
-definition [code func del]: "eq_class.eq (a\<Colon>rat) b \<longleftrightarrow> a - b = 0"
+definition [code del]: "eq_class.eq (a\<Colon>rat) b \<longleftrightarrow> a - b = 0"
 
 instance by default (simp add: eq_rat_def)
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Real/RealDef.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -15,7 +15,7 @@
 
 definition
   realrel   ::  "((preal * preal) * (preal * preal)) set" where
-  [code func del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
+  [code del]: "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
 
 typedef (Real)  real = "UNIV//realrel"
   by (auto simp add: quotient_def)
@@ -23,46 +23,46 @@
 definition
   (** these don't use the overloaded "real" function: users don't see them **)
   real_of_preal :: "preal => real" where
-  [code func del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
+  [code del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})"
 
 instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}"
 begin
 
 definition
-  real_zero_def [code func del]: "0 = Abs_Real(realrel``{(1, 1)})"
+  real_zero_def [code del]: "0 = Abs_Real(realrel``{(1, 1)})"
 
 definition
-  real_one_def [code func del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
+  real_one_def [code del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})"
 
 definition
-  real_add_def [code func del]: "z + w =
+  real_add_def [code del]: "z + w =
        contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
                  { Abs_Real(realrel``{(x+u, y+v)}) })"
 
 definition
-  real_minus_def [code func del]: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
+  real_minus_def [code del]: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
 
 definition
-  real_diff_def [code func del]: "r - (s::real) = r + - s"
+  real_diff_def [code del]: "r - (s::real) = r + - s"
 
 definition
-  real_mult_def [code func del]:
+  real_mult_def [code del]:
     "z * w =
        contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
                  { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
 
 definition
-  real_inverse_def [code func del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
+  real_inverse_def [code del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
 
 definition
-  real_divide_def [code func del]: "R / (S::real) = R * inverse S"
+  real_divide_def [code del]: "R / (S::real) = R * inverse S"
 
 definition
-  real_le_def [code func del]: "z \<le> (w::real) \<longleftrightarrow>
+  real_le_def [code del]: "z \<le> (w::real) \<longleftrightarrow>
     (\<exists>x y u v. x+v \<le> u+y & (x,y) \<in> Rep_Real z & (u,v) \<in> Rep_Real w)"
 
 definition
-  real_less_def [code func del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
+  real_less_def [code del]: "x < (y\<Colon>real) \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
 
 definition
   real_abs_def:  "abs (r::real) = (if r < 0 then - r else r)"
@@ -939,7 +939,7 @@
 begin
 
 definition
-  real_number_of_def [code func del]: "number_of w = real_of_int w"
+  real_number_of_def [code del]: "number_of w = real_of_int w"
 
 instance
   by intro_classes (simp add: real_number_of_def)
diff -r 056255ade52a -r 4e74209f113e src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Real/RealVector.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -308,7 +308,7 @@
 
 definition
   Reals :: "'a::real_algebra_1 set" where
-  [code func del]: "Reals \<equiv> range of_real"
+  [code del]: "Reals \<equiv> range of_real"
 
 notation (xsymbols)
   Reals  ("\<real>")
diff -r 056255ade52a -r 4e74209f113e src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Set.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -324,8 +324,8 @@
 text {* Isomorphisms between predicates and sets. *}
 
 defs
-  mem_def [code func]: "x : S == S x"
-  Collect_def [code func]: "Collect P == P"
+  mem_def [code]: "x : S == S x"
+  Collect_def [code]: "Collect P == P"
 
 defs
   Ball_def:     "Ball A P       == ALL x. x:A --> P(x)"
@@ -2061,7 +2061,7 @@
 
 constdefs
   vimage :: "('a => 'b) => 'b set => 'a set"    (infixr "-`" 90)
-  [code func del]: "f -` B == {x. f x : B}"
+  [code del]: "f -` B == {x. f x : B}"
 
 
 subsubsection {* Basic rules *}
@@ -2156,7 +2156,7 @@
 definition
   contents :: "'a set \<Rightarrow> 'a"
 where
-  [code func del]: "contents X = (THE x. X = {x})"
+  [code del]: "contents X = (THE x. X = {x})"
 
 lemma contents_eq [simp]: "contents {x} = x"
   by (simp add: contents_def)
@@ -2189,22 +2189,22 @@
 
 subsection {* Rudimentary code generation *}
 
-lemma empty_code [code func]: "{} x \<longleftrightarrow> False"
+lemma empty_code [code]: "{} x \<longleftrightarrow> False"
   unfolding empty_def Collect_def ..
 
-lemma UNIV_code [code func]: "UNIV x \<longleftrightarrow> True"
+lemma UNIV_code [code]: "UNIV x \<longleftrightarrow> True"
   unfolding UNIV_def Collect_def ..
 
-lemma insert_code [code func]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
+lemma insert_code [code]: "insert y A x \<longleftrightarrow> y = x \<or> A x"
   unfolding insert_def Collect_def mem_def Un_def by auto
 
-lemma inter_code [code func]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
+lemma inter_code [code]: "(A \<inter> B) x \<longleftrightarrow> A x \<and> B x"
   unfolding Int_def Collect_def mem_def ..
 
-lemma union_code [code func]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
+lemma union_code [code]: "(A \<union> B) x \<longleftrightarrow> A x \<or> B x"
   unfolding Un_def Collect_def mem_def ..
 
-lemma vimage_code [code func]: "(f -` A) x = A (f x)"
+lemma vimage_code [code]: "(f -` A) x = A (f x)"
   unfolding vimage_def Collect_def mem_def ..
 
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/SizeChange/Graphs.thy
--- a/src/HOL/SizeChange/Graphs.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/SizeChange/Graphs.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -67,7 +67,7 @@
   graph_zero_def: "0 = Graph {}" 
 
 definition
-  graph_plus_def [code func del]: "G + H = Graph (dest_graph G \<union> dest_graph H)"
+  graph_plus_def [code del]: "G + H = Graph (dest_graph G \<union> dest_graph H)"
 
 instance proof
   fix x y z :: "('a,'b) graph"
@@ -83,22 +83,22 @@
 begin
 
 definition
-  graph_leq_def [code func del]: "G \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
+  graph_leq_def [code del]: "G \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
 
 definition
-  graph_less_def [code func del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
+  graph_less_def [code del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
 
 definition
-  [code func del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
+  [code del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
 
 definition
-  [code func del]: "sup (G \<Colon> ('a, 'b) graph) H = G + H"
+  [code del]: "sup (G \<Colon> ('a, 'b) graph) H = G + H"
 
 definition
-  Inf_graph_def [code func del]: "Inf = (\<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs)))"
+  Inf_graph_def [code del]: "Inf = (\<lambda>Gs. Graph (\<Inter>(dest_graph ` Gs)))"
 
 definition
-  Sup_graph_def [code func del]: "Sup = (\<lambda>Gs. Graph (\<Union>(dest_graph ` Gs)))"
+  Sup_graph_def [code del]: "Sup = (\<lambda>Gs. Graph (\<Union>(dest_graph ` Gs)))"
 
 instance proof
   fix x y z :: "('a,'b) graph"
@@ -165,7 +165,7 @@
 begin
 
 definition
-  graph_mult_def [code func del]: "G * H = grcomp G H" 
+  graph_mult_def [code del]: "G * H = grcomp G H" 
 
 instance proof
   fix a :: "('a, 'b) graph"
diff -r 056255ade52a -r 4e74209f113e src/HOL/SizeChange/Implementation.thy
--- a/src/HOL/SizeChange/Implementation.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/SizeChange/Implementation.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -122,16 +122,16 @@
 code_modulename SML
   Implementation Graphs
 
-lemma [code func]:
+lemma [code]:
   "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) \<le> H \<longleftrightarrow> dest_graph G \<subseteq> dest_graph H"
   "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
   unfolding graph_leq_def graph_less_def by rule+
 
-lemma [code func]:
+lemma [code]:
   "(G\<Colon>('a\<Colon>eq, 'b\<Colon>eq) graph) + H = Graph (dest_graph G \<union> dest_graph H)"
   unfolding graph_plus_def ..
 
-lemma [code func]:
+lemma [code]:
   "(G\<Colon>('a\<Colon>eq, 'b\<Colon>{eq, times}) graph) * H = grcomp G H"
   unfolding graph_mult_def ..
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/Tools/ComputeHOL.thy
--- a/src/HOL/Tools/ComputeHOL.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Tools/ComputeHOL.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -1,5 +1,5 @@
 theory ComputeHOL
-imports Main "~~/src/Tools/Compute_Oracle/Compute_Oracle"
+imports Complex_Main "~~/src/Tools/Compute_Oracle/Compute_Oracle"
 begin
 
 lemma Trueprop_eq_eq: "Trueprop X == (X == True)" by (simp add: atomize_eq)
diff -r 056255ade52a -r 4e74209f113e src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Wellfounded.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -40,7 +40,7 @@
      (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
 
   wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
-  [code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
+  [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
 
 abbreviation acyclicP :: "('a => 'a => bool) => bool" where
   "acyclicP r == acyclic {(x, y). r x y}"
@@ -840,10 +840,10 @@
 
 setup Size.setup
 
-lemma size_bool [code func]:
+lemma size_bool [code]:
   "size (b\<Colon>bool) = 0" by (cases b) auto
 
-lemma nat_size [simp, code func]: "size (n\<Colon>nat) = n"
+lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
   by (induct n) simp_all
 
 declare "prod.size" [noatp]
diff -r 056255ade52a -r 4e74209f113e src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Word/BinGeneral.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -129,7 +129,7 @@
 subsection {* Destructors for binary integers *}
 
 definition bin_rl :: "int \<Rightarrow> int \<times> bit" where 
-  [code func del]: "bin_rl w = (THE (r, l). w = r BIT l)"
+  [code del]: "bin_rl w = (THE (r, l). w = r BIT l)"
 
 lemma bin_rl_char: "(bin_rl w = (r, l)) = (r BIT l = w)"
   apply (unfold bin_rl_def)
@@ -139,10 +139,10 @@
   done
 
 definition
-  bin_rest_def [code func del]: "bin_rest w = fst (bin_rl w)"
+  bin_rest_def [code del]: "bin_rest w = fst (bin_rl w)"
 
 definition
-  bin_last_def [code func del] : "bin_last w = snd (bin_rl w)"
+  bin_last_def [code del] : "bin_last w = snd (bin_rl w)"
 
 primrec bin_nth where
   Z: "bin_nth w 0 = (bin_last w = bit.B1)"
@@ -159,7 +159,7 @@
   "bin_rl (r BIT b) = (r, b)"
   unfolding bin_rl_char by simp_all
 
-declare bin_rl_simps(1-4) [code func]
+declare bin_rl_simps(1-4) [code]
 
 lemmas bin_rl_simp [simp] = iffD1 [OF bin_rl_char bin_rl]
 
@@ -212,7 +212,7 @@
   "bin_rest (w BIT b) = w"
   unfolding bin_rest_def by auto
 
-declare bin_rest_simps(1-4) [code func]
+declare bin_rest_simps(1-4) [code]
 
 lemma bin_last_simps [simp]: 
   "bin_last Int.Pls = bit.B0"
@@ -222,7 +222,7 @@
   "bin_last (w BIT b) = b"
   unfolding bin_last_def by auto
 
-declare bin_last_simps(1-4) [code func]
+declare bin_last_simps(1-4) [code]
 
 lemma bin_r_l_extras [simp]:
   "bin_last 0 = bit.B0"
@@ -403,7 +403,7 @@
 subsection {* Truncating binary integers *}
 
 definition
-  bin_sign_def [code func del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
+  bin_sign_def [code del] : "bin_sign = bin_rec Int.Pls Int.Min (%w b s. s)"
 
 lemma bin_sign_simps [simp]:
   "bin_sign Int.Pls = Int.Pls"
@@ -413,7 +413,7 @@
   "bin_sign (w BIT b) = bin_sign w"
   unfolding bin_sign_def by (auto simp: bin_rec_simps)
 
-declare bin_sign_simps(1-4) [code func]
+declare bin_sign_simps(1-4) [code]
 
 lemma bin_sign_rest [simp]: 
   "bin_sign (bin_rest w) = (bin_sign w)"
diff -r 056255ade52a -r 4e74209f113e src/HOL/Word/BinOperations.thy
--- a/src/HOL/Word/BinOperations.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Word/BinOperations.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -21,19 +21,19 @@
 begin
 
 definition
-  int_not_def [code func del]: "bitNOT = bin_rec Int.Min Int.Pls 
+  int_not_def [code del]: "bitNOT = bin_rec Int.Min Int.Pls 
     (\<lambda>w b s. s BIT (NOT b))"
 
 definition
-  int_and_def [code func del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y) 
+  int_and_def [code del]: "bitAND = bin_rec (\<lambda>x. Int.Pls) (\<lambda>y. y) 
     (\<lambda>w b s y. s (bin_rest y) BIT (b AND bin_last y))"
 
 definition
-  int_or_def [code func del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min) 
+  int_or_def [code del]: "bitOR = bin_rec (\<lambda>x. x) (\<lambda>y. Int.Min) 
     (\<lambda>w b s y. s (bin_rest y) BIT (b OR bin_last y))"
 
 definition
-  int_xor_def [code func del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT 
+  int_xor_def [code del]: "bitXOR = bin_rec (\<lambda>x. x) bitNOT 
     (\<lambda>w b s y. s (bin_rest y) BIT (b XOR bin_last y))"
 
 instance ..
@@ -48,13 +48,13 @@
   "NOT (w BIT b) = (NOT w) BIT (NOT b)"
   unfolding int_not_def by (simp_all add: bin_rec_simps)
 
-declare int_not_simps(1-4) [code func]
+declare int_not_simps(1-4) [code]
 
-lemma int_xor_Pls [simp, code func]: 
+lemma int_xor_Pls [simp, code]: 
   "Int.Pls XOR x = x"
   unfolding int_xor_def by (simp add: bin_rec_PM)
 
-lemma int_xor_Min [simp, code func]: 
+lemma int_xor_Min [simp, code]: 
   "Int.Min XOR x = NOT x"
   unfolding int_xor_def by (simp add: bin_rec_PM)
 
@@ -69,7 +69,7 @@
   apply (simp add: int_not_simps [symmetric])
   done
 
-lemma int_xor_Bits2 [simp, code func]: 
+lemma int_xor_Bits2 [simp, code]: 
   "(Int.Bit0 x) XOR (Int.Bit0 y) = Int.Bit0 (x XOR y)"
   "(Int.Bit0 x) XOR (Int.Bit1 y) = Int.Bit1 (x XOR y)"
   "(Int.Bit1 x) XOR (Int.Bit0 y) = Int.Bit1 (x XOR y)"
@@ -85,16 +85,16 @@
    apply clarsimp+
   done
 
-lemma int_xor_extra_simps [simp, code func]:
+lemma int_xor_extra_simps [simp, code]:
   "w XOR Int.Pls = w"
   "w XOR Int.Min = NOT w"
   using int_xor_x_simps' by simp_all
 
-lemma int_or_Pls [simp, code func]: 
+lemma int_or_Pls [simp, code]: 
   "Int.Pls OR x = x"
   by (unfold int_or_def) (simp add: bin_rec_PM)
   
-lemma int_or_Min [simp, code func]:
+lemma int_or_Min [simp, code]:
   "Int.Min OR x = Int.Min"
   by (unfold int_or_def) (simp add: bin_rec_PM)
 
@@ -102,7 +102,7 @@
   "(x BIT b) OR (y BIT c) = (x OR y) BIT (b OR c)"
   unfolding int_or_def by (simp add: bin_rec_simps)
 
-lemma int_or_Bits2 [simp, code func]: 
+lemma int_or_Bits2 [simp, code]: 
   "(Int.Bit0 x) OR (Int.Bit0 y) = Int.Bit0 (x OR y)"
   "(Int.Bit0 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
   "(Int.Bit1 x) OR (Int.Bit0 y) = Int.Bit1 (x OR y)"
@@ -118,16 +118,16 @@
    apply clarsimp+
   done
 
-lemma int_or_extra_simps [simp, code func]:
+lemma int_or_extra_simps [simp, code]:
   "w OR Int.Pls = w"
   "w OR Int.Min = Int.Min"
   using int_or_x_simps' by simp_all
 
-lemma int_and_Pls [simp, code func]:
+lemma int_and_Pls [simp, code]:
   "Int.Pls AND x = Int.Pls"
   unfolding int_and_def by (simp add: bin_rec_PM)
 
-lemma int_and_Min [simp, code func]:
+lemma int_and_Min [simp, code]:
   "Int.Min AND x = x"
   unfolding int_and_def by (simp add: bin_rec_PM)
 
@@ -135,7 +135,7 @@
   "(x BIT b) AND (y BIT c) = (x AND y) BIT (b AND c)" 
   unfolding int_and_def by (simp add: bin_rec_simps)
 
-lemma int_and_Bits2 [simp, code func]: 
+lemma int_and_Bits2 [simp, code]: 
   "(Int.Bit0 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
   "(Int.Bit0 x) AND (Int.Bit1 y) = Int.Bit0 (x AND y)"
   "(Int.Bit1 x) AND (Int.Bit0 y) = Int.Bit0 (x AND y)"
@@ -151,7 +151,7 @@
    apply clarsimp+
   done
 
-lemma int_and_extra_simps [simp, code func]:
+lemma int_and_extra_simps [simp, code]:
   "w AND Int.Pls = Int.Pls"
   "w AND Int.Min = w"
   using int_and_x_simps' by simp_all
diff -r 056255ade52a -r 4e74209f113e src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Word/WordDefinition.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -30,7 +30,7 @@
         only difference in these is the type class *}
   word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word"
 where
-  [code func del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
+  [code del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
 
 code_datatype word_of_int
 
@@ -96,9 +96,9 @@
 
 subsection  "Arithmetic operations"
 
-declare uint_def [code func del]
+declare uint_def [code del]
 
-lemma [code func]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = bintrunc (len_of TYPE('a)) w"
+lemma [code]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = bintrunc (len_of TYPE('a)) w"
   by (auto simp add: uint_def word_of_int_def intro!: Abs_word_inverse)
     (insert range_bintrunc, auto)
 
diff -r 056255ade52a -r 4e74209f113e src/HOL/ex/Codegenerator_Pretty.thy
--- a/src/HOL/ex/Codegenerator_Pretty.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/ex/Codegenerator_Pretty.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -9,7 +9,7 @@
 imports ExecutableContent Code_Char Efficient_Nat
 begin
 
-declare isnorm.simps [code func del]
+declare isnorm.simps [code del]
 
 ML {* (*FIXME get rid of this*)
 nonfix union;
diff -r 056255ade52a -r 4e74209f113e src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/ex/NormalForm.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -12,7 +12,7 @@
 lemma "p \<longrightarrow> True" by normalization
 declare disj_assoc [code nbe]
 lemma "((P | Q) | R) = (P | (Q | R))" by normalization
-declare disj_assoc [code func del]
+declare disj_assoc [code del]
 lemma "0 + (n::nat) = n" by normalization
 lemma "0 + Suc n = Suc n" by normalization
 lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
diff -r 056255ade52a -r 4e74209f113e src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/ex/Numeral.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -74,19 +74,19 @@
 begin
 
 definition one_num :: num where
-  [code func del]: "1 = num_of_nat 1"
+  [code del]: "1 = num_of_nat 1"
 
 definition plus_num :: "num \<Rightarrow> num \<Rightarrow> num" where
-  [code func del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
+  [code del]: "m + n = num_of_nat (nat_of_num m + nat_of_num n)"
 
 definition times_num :: "num \<Rightarrow> num \<Rightarrow> num" where
-  [code func del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
+  [code del]: "m * n = num_of_nat (nat_of_num m * nat_of_num n)"
 
 definition Dig0 :: "num \<Rightarrow> num" where
-  [code func del]: "Dig0 n = n + n"
+  [code del]: "Dig0 n = n + n"
 
 definition Dig1 :: "num \<Rightarrow> num" where
-  [code func del]: "Dig1 n = n + n + 1"
+  [code del]: "Dig1 n = n + n + 1"
 
 instance proof
 qed (simp_all add: one_num_def plus_num_def times_num_def
@@ -503,10 +503,10 @@
 begin
 
 definition less_eq_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
-  [code func del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
+  [code del]: "m \<le> n \<longleftrightarrow> nat_of_num m \<le> nat_of_num n"
 
 definition less_num :: "num \<Rightarrow> num \<Rightarrow> bool" where
-  [code func del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
+  [code del]: "m < n \<longleftrightarrow> nat_of_num m < nat_of_num n"
 
 instance proof
 qed (auto simp add: less_eq_num_def less_num_def
@@ -768,10 +768,10 @@
 lemmas [code inline] = Pls_def [symmetric] Mns_def [symmetric]
 
 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
-  [simp, code func del]: "sub m n = (of_num m - of_num n)"
+  [simp, code del]: "sub m n = (of_num m - of_num n)"
 
 definition dup :: "int \<Rightarrow> int" where
-  [code func del]: "dup k = 2 * k"
+  [code del]: "dup k = 2 * k"
 
 lemma Dig_sub [code]:
   "sub 1 1 = 0"
@@ -794,7 +794,7 @@
   "dup (Mns n) = Mns (Dig0 n)"
   by (simp_all add: dup_def of_num.simps)
   
-lemma [code func, code func del]:
+lemma [code, code del]:
   "(1 :: int) = 1"
   "(op + :: int \<Rightarrow> int \<Rightarrow> int) = op +"
   "(uminus :: int \<Rightarrow> int) = uminus"
diff -r 056255ade52a -r 4e74209f113e src/HOL/ex/Random.thy
--- a/src/HOL/ex/Random.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/ex/Random.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -124,7 +124,7 @@
 definition
   select_default :: "index \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> seed \<Rightarrow> 'a \<times> seed"
 where
-  [code func del]: "select_default k x y = (do
+  [code del]: "select_default k x y = (do
      l \<leftarrow> range k;
      return (if l + 1 < k then x else y)
    done)"
diff -r 056255ade52a -r 4e74209f113e src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/Pure/Isar/code.ML	Fri Oct 10 06:45:53 2008 +0200
@@ -96,12 +96,10 @@
 
 fun add_attribute (attr as (name, _)) =
   let
-    fun add_parser ("", parser) attrs = attrs @ [("", parser)]
+    fun add_parser ("", parser) attrs = attrs |> rev |> AList.update (op =) ("", parser) |> rev
       | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
-    fun error "" = error ("Code attribute already declared")
-      | error name = error ("Code attribute " ^ name ^ " already declared")
-  in CodeAttr.map (fn attrs => if AList.defined (op =) attrs name
-    then error name else add_parser attr attrs)
+  in CodeAttr.map (fn attrs => if not (name = "") andalso AList.defined (op =) attrs name
+    then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs)
   end;
 
 val _ =
@@ -637,7 +635,7 @@
         || Scan.succeed (mk_attribute add))
   in
     TypeInterpretation.init
-    #> add_del_attribute ("func", (add_eqn, del_eqn))
+    #> add_del_attribute ("", (add_eqn, del_eqn))
     #> add_simple_attribute ("nbe", add_nonlinear_eqn)
     #> add_del_attribute ("inline", (add_inline, del_inline))
     #> add_del_attribute ("post", (add_post, del_post))