# HG changeset patch
# User haftmann
# Date 1247561803 -7200
# Node ID fafefd0b341cd4d884538a96adf79f18e1adb24e
# Parent  1d93369079c4a635ac6344c934655a837edaa079# Parent  6f07563dc8a97b15b4c923c367d8c87b9657f571
merged

diff -r 1d93369079c4 -r fafefd0b341c CONTRIBUTORS
--- a/CONTRIBUTORS	Mon Jul 13 19:07:05 2009 +0200
+++ b/CONTRIBUTORS	Tue Jul 14 10:56:43 2009 +0200
@@ -7,6 +7,12 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* July 2009: Florian Haftmann, TUM
+  New quickcheck implementation using new code generator
+
+* July 2009: Florian Haftmann, TUM
+  HOL/Library/FSet: an explicit type of sets; finite sets ready to use for code generation
+
 * June 2009: Andreas Lochbihler, Uni Karlsruhe
   HOL/Library/Fin_Fun: almost everywhere constant functions
 
diff -r 1d93369079c4 -r fafefd0b341c NEWS
--- a/NEWS	Mon Jul 13 19:07:05 2009 +0200
+++ b/NEWS	Tue Jul 14 10:56:43 2009 +0200
@@ -18,6 +18,16 @@
 
 *** HOL ***
 
+* Code generator attributes follow the usual underscore convention:
+    code_unfold     replaces    code unfold
+    code_post       replaces    code post
+    etc.
+  INCOMPATIBILITY.
+
+* New quickcheck implementation using new code generator.
+
+* New type class boolean_algebra.
+
 * Class semiring_div requires superclass no_zero_divisors and proof of
 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
diff -r 1d93369079c4 -r fafefd0b341c doc-src/Codegen/Thy/ML.thy
--- a/doc-src/Codegen/Thy/ML.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/doc-src/Codegen/Thy/ML.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -78,8 +78,7 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML Code.read_const: "theory -> string -> string"} \\
-  @{index_ML Code.rewrite_eqn: "simpset -> thm -> thm"} \\
+  @{index_ML Code.read_const: "theory -> string -> string"}
   \end{mldecls}
 
   \begin{description}
@@ -87,11 +86,6 @@
   \item @{ML Code.read_const}~@{text thy}~@{text s}
      reads a constant as a concrete term expression @{text s}.
 
-  \item @{ML Code.rewrite_eqn}~@{text ss}~@{text thm}
-     rewrites a code equation @{text thm} with a simpset @{text ss};
-     only arguments and right hand side are rewritten,
-     not the head of the code equation.
-
   \end{description}
 
 *}
diff -r 1d93369079c4 -r fafefd0b341c doc-src/Codegen/Thy/Program.thy
--- a/doc-src/Codegen/Thy/Program.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/doc-src/Codegen/Thy/Program.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -153,14 +153,14 @@
   out: \emph{preprocessing}.  In essence, the preprocessor
   consists of two components: a \emph{simpset} and \emph{function transformers}.
 
-  The \emph{simpset} allows to employ the full generality of the Isabelle
-  simplifier.  Due to the interpretation of theorems
-  as code equations, rewrites are applied to the right
-  hand side and the arguments of the left hand side of an
-  equation, but never to the constant heading the left hand side.
-  An important special case are \emph{inline theorems} which may be
-  declared and undeclared using the
-  \emph{code inline} or \emph{code inline del} attribute respectively.
+  The \emph{simpset} allows to employ the full generality of the
+  Isabelle simplifier.  Due to the interpretation of theorems as code
+  equations, rewrites are applied to the right hand side and the
+  arguments of the left hand side of an equation, but never to the
+  constant heading the left hand side.  An important special case are
+  \emph{unfold theorems} which may be declared and undeclared using
+  the @{attribute code_unfold} or \emph{@{attribute code_unfold} del}
+  attribute respectively.
 
   Some common applications:
 *}
@@ -173,21 +173,21 @@
      \item replacing non-executable constructs by executable ones:
 *}     
 
-lemma %quote [code inline]:
+lemma %quote [code_inline]:
   "x \<in> set xs \<longleftrightarrow> x mem xs" by (induct xs) simp_all
 
 text {*
      \item eliminating superfluous constants:
 *}
 
-lemma %quote [code inline]:
+lemma %quote [code_inline]:
   "1 = Suc 0" by simp
 
 text {*
      \item replacing executable but inconvenient constructs:
 *}
 
-lemma %quote [code inline]:
+lemma %quote [code_inline]:
   "xs = [] \<longleftrightarrow> List.null xs" by (induct xs) simp_all
 
 text_raw {*
@@ -210,10 +210,10 @@
   on code equations.
 
   \begin{warn}
-    The attribute \emph{code unfold}
-    associated with the @{text "SML code generator"} also applies to
-    the @{text "generic code generator"}:
-    \emph{code unfold} implies \emph{code inline}.
+
+    Attribute @{attribute code_unfold} also applies to the
+    preprocessor of the ancient @{text "SML code generator"}; in case
+    this is not what you intend, use @{attribute code_inline} instead.
   \end{warn}
 *}
 
diff -r 1d93369079c4 -r fafefd0b341c doc-src/Codegen/Thy/document/ML.tex
--- a/doc-src/Codegen/Thy/document/ML.tex	Mon Jul 13 19:07:05 2009 +0200
+++ b/doc-src/Codegen/Thy/document/ML.tex	Tue Jul 14 10:56:43 2009 +0200
@@ -124,8 +124,7 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string| \\
-  \indexdef{}{ML}{Code.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\
+  \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string|
   \end{mldecls}
 
   \begin{description}
@@ -133,11 +132,6 @@
   \item \verb|Code.read_const|~\isa{thy}~\isa{s}
      reads a constant as a concrete term expression \isa{s}.
 
-  \item \verb|Code.rewrite_eqn|~\isa{ss}~\isa{thm}
-     rewrites a code equation \isa{thm} with a simpset \isa{ss};
-     only arguments and right hand side are rewritten,
-     not the head of the code equation.
-
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
diff -r 1d93369079c4 -r fafefd0b341c doc-src/Codegen/Thy/document/Program.tex
--- a/doc-src/Codegen/Thy/document/Program.tex	Mon Jul 13 19:07:05 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Program.tex	Tue Jul 14 10:56:43 2009 +0200
@@ -395,14 +395,14 @@
   out: \emph{preprocessing}.  In essence, the preprocessor
   consists of two components: a \emph{simpset} and \emph{function transformers}.
 
-  The \emph{simpset} allows to employ the full generality of the Isabelle
-  simplifier.  Due to the interpretation of theorems
-  as code equations, rewrites are applied to the right
-  hand side and the arguments of the left hand side of an
-  equation, but never to the constant heading the left hand side.
-  An important special case are \emph{inline theorems} which may be
-  declared and undeclared using the
-  \emph{code inline} or \emph{code inline del} attribute respectively.
+  The \emph{simpset} allows to employ the full generality of the
+  Isabelle simplifier.  Due to the interpretation of theorems as code
+  equations, rewrites are applied to the right hand side and the
+  arguments of the left hand side of an equation, but never to the
+  constant heading the left hand side.  An important special case are
+  \emph{unfold theorems} which may be declared and undeclared using
+  the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del}
+  attribute respectively.
 
   Some common applications:%
 \end{isamarkuptext}%
@@ -421,7 +421,7 @@
 %
 \isatagquote
 \isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ x\ mem\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
 \endisatagquote
@@ -442,7 +442,7 @@
 %
 \isatagquote
 \isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ simp%
 \endisatagquote
@@ -463,7 +463,7 @@
 %
 \isatagquote
 \isacommand{lemma}\isamarkupfalse%
-\ {\isacharbrackleft}code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
+\ {\isacharbrackleft}code{\isacharunderscore}inline{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}induct\ xs{\isacharparenright}\ simp{\isacharunderscore}all%
 \endisatagquote
@@ -491,10 +491,10 @@
   on code equations.
 
   \begin{warn}
-    The attribute \emph{code unfold}
-    associated with the \isa{SML\ code\ generator} also applies to
-    the \isa{generic\ code\ generator}:
-    \emph{code unfold} implies \emph{code inline}.
+
+    Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
+    preprocessor of the ancient \isa{SML\ code\ generator}; in case
+    this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead.
   \end{warn}%
 \end{isamarkuptext}%
 \isamarkuptrue%
diff -r 1d93369079c4 -r fafefd0b341c doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -1190,7 +1190,13 @@
     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     ;
 
-    'code' ( 'inline' ) ? ( 'del' ) ?
+    'code' ( 'del' ) ?
+    ;
+
+    'code_unfold' ( 'del' ) ?
+    ;
+
+    'code_post' ( 'del' ) ?
     ;
   \end{rail}
 
@@ -1280,11 +1286,15 @@
   generation.  Usually packages introducing code equations provide
   a reasonable default setup for selection.
 
-  \item @{attribute (HOL) code}~@{text inline} declares (or with
+  \item @{attribute (HOL) code_inline} declares (or with
   option ``@{text "del"}'' removes) inlining theorems which are
   applied as rewrite rules to any code equation during
   preprocessing.
 
+  \item @{attribute (HOL) code_post} declares (or with
+  option ``@{text "del"}'' removes) theorems which are
+  applied as rewrite rules to any result of an evaluation.
+
   \item @{command (HOL) "print_codesetup"} gives an overview on
   selected code equations and code generator datatypes.
 
diff -r 1d93369079c4 -r fafefd0b341c doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Jul 13 19:07:05 2009 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jul 14 10:56:43 2009 +0200
@@ -1201,7 +1201,13 @@
     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     ;
 
-    'code' ( 'inline' ) ? ( 'del' ) ?
+    'code' ( 'del' ) ?
+    ;
+
+    'code_unfold' ( 'del' ) ?
+    ;
+
+    'code_post' ( 'del' ) ?
     ;
   \end{rail}
 
@@ -1288,11 +1294,15 @@
   generation.  Usually packages introducing code equations provide
   a reasonable default setup for selection.
 
-  \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{inline} declares (or with
+  \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with
   option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
   applied as rewrite rules to any code equation during
   preprocessing.
 
+  \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with
+  option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are
+  applied as rewrite rules to any result of an evaluation.
+
   \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
   selected code equations and code generator datatypes.
 
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Code_Eval.thy
--- a/src/HOL/Code_Eval.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Code_Eval.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -32,7 +32,7 @@
   \<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
   "valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
 
-lemma valapp_code [code, code inline]:
+lemma valapp_code [code, code_inline]:
   "valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
   by (simp only: valapp_def fst_conv snd_conv)
 
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Code_Numeral.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -176,16 +176,16 @@
 
 end
 
-lemma zero_code_numeral_code [code inline, code]:
+lemma zero_code_numeral_code [code_inline, code]:
   "(0\<Colon>code_numeral) = Numeral0"
   by (simp add: number_of_code_numeral_def Pls_def)
-lemma [code post]: "Numeral0 = (0\<Colon>code_numeral)"
+lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
   using zero_code_numeral_code ..
 
-lemma one_code_numeral_code [code inline, code]:
+lemma one_code_numeral_code [code_inline, code]:
   "(1\<Colon>code_numeral) = Numeral1"
   by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
-lemma [code post]: "Numeral1 = (1\<Colon>code_numeral)"
+lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)"
   using one_code_numeral_code ..
 
 lemma plus_code_numeral_code [code nbe]:
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Divides.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -131,7 +131,7 @@
   note that ultimately show thesis by blast
 qed
 
-lemma dvd_eq_mod_eq_0 [code unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma dvd_eq_mod_eq_0 [code_unfold]: "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
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/HOL.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -1787,7 +1787,7 @@
   assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
 begin
 
-lemma eq [code unfold, code inline del]: "eq = (op =)"
+lemma eq [code_unfold, code_inline del]: "eq = (op =)"
   by (rule ext eq_equals)+
 
 lemma eq_refl: "eq x x \<longleftrightarrow> True"
@@ -1796,7 +1796,7 @@
 lemma equals_eq: "(op =) \<equiv> eq"
   by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
 
-declare equals_eq [symmetric, code post]
+declare equals_eq [symmetric, code_post]
 
 end
 
@@ -1847,7 +1847,7 @@
 
 lemmas [code] = Let_def if_True if_False
 
-lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
+lemmas [code, code_unfold, symmetric, code_post] = imp_conv_disj
 
 instantiation itself :: (type) eq
 begin
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -283,7 +283,7 @@
 where
   [code del]: "raise_exc e = raise []"
 
-lemma raise_raise_exc [code, 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 1d93369079c4 -r fafefd0b341c src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Int.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -650,11 +650,11 @@
 
 text {* Removal of leading zeroes *}
 
-lemma Bit0_Pls [simp, code post]:
+lemma Bit0_Pls [simp, code_post]:
   "Bit0 Pls = Pls"
   unfolding numeral_simps by simp
 
-lemma Bit1_Min [simp, code post]:
+lemma Bit1_Min [simp, code_post]:
   "Bit1 Min = Min"
   unfolding numeral_simps by simp
 
@@ -2126,11 +2126,11 @@
 
 hide (open) const nat_aux
 
-lemma zero_is_num_zero [code, 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, code inline, symmetric, code post]:
+lemma one_is_num_one [code, code_inline, symmetric, code_post]:
   "(1\<Colon>int) = Numeral1" 
   by simp
 
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/IntDiv.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -36,7 +36,7 @@
 
 text{*algorithm for the general case @{term "b\<noteq>0"}*}
 definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
-  [code inline]: "negateSnd = apsnd uminus"
+  [code_inline]: "negateSnd = apsnd uminus"
 
 definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
     --{*The full division algorithm considers all possible signs for a, b
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Library/Code_Char_chr.thy
--- a/src/HOL/Library/Code_Char_chr.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Library/Code_Char_chr.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -24,11 +24,11 @@
 
 lemmas [code del] = char.recs char.cases char.size
 
-lemma [code, 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, 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)
 
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -26,15 +26,15 @@
 
 code_datatype number_nat_inst.number_of_nat
 
-lemma zero_nat_code [code, code inline]:
+lemma zero_nat_code [code, code_inline]:
   "0 = (Numeral0 :: nat)"
   by simp
-lemmas [code post] = zero_nat_code [symmetric]
+lemmas [code_post] = zero_nat_code [symmetric]
 
-lemma one_nat_code [code, code inline]:
+lemma one_nat_code [code, code_inline]:
   "1 = (Numeral1 :: nat)"
   by simp
-lemmas [code post] = one_nat_code [symmetric]
+lemmas [code_post] = one_nat_code [symmetric]
 
 lemma Suc_code [code]:
   "Suc n = n + 1"
@@ -89,7 +89,7 @@
   expression:
 *}
 
-lemma [code, code unfold]:
+lemma [code, code_unfold]:
   "nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
   by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc)
 
@@ -302,7 +302,7 @@
   Natural numerals.
 *}
 
-lemma [code inline, symmetric, code post]:
+lemma [code_inline, symmetric, code_post]:
   "nat (number_of i) = number_nat_inst.number_of_nat i"
   -- {* this interacts as desired with @{thm nat_number_of_def} *}
   by (simp add: number_nat_inst.number_of_nat)
@@ -335,9 +335,9 @@
   "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
   unfolding nat_number_of_def number_of_is_id neg_def by simp
 
-lemma of_nat_int [code unfold]:
+lemma of_nat_int [code_unfold]:
   "of_nat = int" by (simp add: int_def)
-declare of_nat_int [symmetric, code post]
+declare of_nat_int [symmetric, code_post]
 
 code_const int
   (SML "_")
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -15,7 +15,7 @@
 definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   "subset = op \<le>"
 
-declare subset_def [symmetric, code unfold]
+declare subset_def [symmetric, code_unfold]
 
 lemma [code]:
   "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
@@ -25,7 +25,7 @@
   [code del]: "eq_set = op ="
 
 (* FIXME allow for Stefan's code generator:
-declare set_eq_subset[code unfold]
+declare set_eq_subset[code_unfold]
 *)
 
 lemma [code]:
@@ -40,7 +40,7 @@
 
 subsection {* Rewrites for primitive operations *}
 
-declare List_Set.project_def [symmetric, code unfold]
+declare List_Set.project_def [symmetric, code_unfold]
 
 
 subsection {* code generator setup *}
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Library/Float.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -19,7 +19,7 @@
   "of_float (Float a b) = real a * pow2 b"
 
 defs (overloaded)
-  real_of_float_def [code unfold]: "real == of_float"
+  real_of_float_def [code_unfold]: "real == of_float"
 
 primrec mantissa :: "float \<Rightarrow> int" where
   "mantissa (Float a b) = a"
@@ -42,7 +42,7 @@
 instance ..
 end
 
-lemma number_of_float_Float [code inline, symmetric, code post]:
+lemma number_of_float_Float [code_inline, symmetric, code_post]:
   "number_of k = Float (number_of k) 0"
   by (simp add: number_of_float_def number_of_is_id)
 
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Library/Fraction_Field.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -93,10 +93,10 @@
 begin
 
 definition
-  Zero_fract_def [code, code unfold]: "0 = Fract 0 1"
+  Zero_fract_def [code, code_unfold]: "0 = Fract 0 1"
 
 definition
-  One_fract_def [code, code unfold]: "1 = Fract 1 1"
+  One_fract_def [code, code_unfold]: "1 = Fract 1 1"
 
 definition
   add_fract_def [code del]:
@@ -196,14 +196,14 @@
 lemma Fract_of_nat_eq: "Fract (of_nat k) 1 = of_nat k"
   by (rule of_nat_fract [symmetric])
 
-lemma fract_collapse [code post]:
+lemma fract_collapse [code_post]:
   "Fract 0 k = 0"
   "Fract 1 1 = 1"
   "Fract k 0 = 0"
   by (cases "k = 0")
     (simp_all add: Zero_fract_def One_fract_def eq_fract Fract_def)
 
-lemma fract_expand [code unfold]:
+lemma fract_expand [code_unfold]:
   "0 = Fract 0 1"
   "1 = Fract 1 1"
   by (simp_all add: fract_collapse)
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -40,10 +40,10 @@
   "0 = Fin 0"
 
 definition
-  [code inline]: "1 = Fin 1"
+  [code_inline]: "1 = Fin 1"
 
 definition
-  [code inline, code del]: "number_of k = Fin (number_of k)"
+  [code_inline, code del]: "number_of k = Fin (number_of k)"
 
 instance ..
 
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Library/Polynomial.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -1505,7 +1505,7 @@
 
 code_datatype "0::'a::zero poly" pCons
 
-declare pCons_0_0 [code post]
+declare pCons_0_0 [code_post]
 
 instantiation poly :: ("{zero,eq}") eq
 begin
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/List.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -2076,7 +2076,7 @@
 by(induct xs) simp_all
 
 text{* For efficient code generation: avoid intermediate list. *}
-lemma foldl_map[code unfold]:
+lemma foldl_map[code_unfold]:
   "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
 by(induct xs arbitrary:a) simp_all
 
@@ -2198,7 +2198,7 @@
 
 text{* For efficient code generation ---
        @{const listsum} is not tail recursive but @{const foldl} is. *}
-lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs"
+lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
 by(simp add:listsum_foldr foldl_foldr1)
 
 lemma distinct_listsum_conv_Setsum:
@@ -3746,32 +3746,32 @@
   show ?case by (induct xs) (auto simp add: Cons aux)
 qed
 
-lemma mem_iff [code post]:
+lemma mem_iff [code_post]:
   "x mem xs \<longleftrightarrow> x \<in> set xs"
 by (induct xs) auto
 
-lemmas in_set_code [code unfold] = mem_iff [symmetric]
+lemmas in_set_code [code_unfold] = mem_iff [symmetric]
 
 lemma empty_null:
   "xs = [] \<longleftrightarrow> null xs"
 by (cases xs) simp_all
 
-lemma [code inline]:
+lemma [code_inline]:
   "eq_class.eq xs [] \<longleftrightarrow> null xs"
 by (simp add: eq empty_null)
 
-lemmas null_empty [code post] =
+lemmas null_empty [code_post] =
   empty_null [symmetric]
 
 lemma list_inter_conv:
   "set (list_inter xs ys) = set xs \<inter> set ys"
 by (induct xs) auto
 
-lemma list_all_iff [code post]:
+lemma list_all_iff [code_post]:
   "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
 by (induct xs) auto
 
-lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
+lemmas list_ball_code [code_unfold] = list_all_iff [symmetric]
 
 lemma list_all_append [simp]:
   "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
@@ -3785,11 +3785,11 @@
   "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
   unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
 
-lemma list_ex_iff [code post]:
+lemma list_ex_iff [code_post]:
   "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
 by (induct xs) simp_all
 
-lemmas list_bex_code [code unfold] =
+lemmas list_bex_code [code_unfold] =
   list_ex_iff [symmetric]
 
 lemma list_ex_length:
@@ -3804,7 +3804,7 @@
   "map_filter f P xs = map f (filter P xs)"
 by (induct xs) auto
 
-lemma length_remdups_length_unique [code inline]:
+lemma length_remdups_length_unique [code_inline]:
   "length (remdups xs) = length_unique xs"
   by (induct xs) simp_all
 
@@ -3813,43 +3813,43 @@
 
 text {* Code for bounded quantification and summation over nats. *}
 
-lemma atMost_upto [code unfold]:
+lemma atMost_upto [code_unfold]:
   "{..n} = set [0..<Suc n]"
 by auto
 
-lemma atLeast_upt [code unfold]:
+lemma atLeast_upt [code_unfold]:
   "{..<n} = set [0..<n]"
 by auto
 
-lemma greaterThanLessThan_upt [code unfold]:
+lemma greaterThanLessThan_upt [code_unfold]:
   "{n<..<m} = set [Suc n..<m]"
 by auto
 
-lemma atLeastLessThan_upt [code unfold]:
+lemma atLeastLessThan_upt [code_unfold]:
   "{n..<m} = set [n..<m]"
 by auto
 
-lemma greaterThanAtMost_upt [code unfold]:
+lemma greaterThanAtMost_upt [code_unfold]:
   "{n<..m} = set [Suc n..<Suc m]"
 by auto
 
-lemma atLeastAtMost_upt [code unfold]:
+lemma atLeastAtMost_upt [code_unfold]:
   "{n..m} = set [n..<Suc m]"
 by auto
 
-lemma all_nat_less_eq [code unfold]:
+lemma all_nat_less_eq [code_unfold]:
   "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
 by auto
 
-lemma ex_nat_less_eq [code unfold]:
+lemma ex_nat_less_eq [code_unfold]:
   "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
 by auto
 
-lemma all_nat_less [code unfold]:
+lemma all_nat_less [code_unfold]:
   "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
 by auto
 
-lemma ex_nat_less [code unfold]:
+lemma ex_nat_less [code_unfold]:
   "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
 by auto
 
@@ -3857,30 +3857,30 @@
   "distinct xs \<Longrightarrow> setsum f (set xs) = listsum (map f xs)"
 by (induct xs) simp_all
 
-lemma setsum_set_upt_conv_listsum [code unfold]:
+lemma setsum_set_upt_conv_listsum [code_unfold]:
   "setsum f (set [m..<n]) = listsum (map f [m..<n])"
 by (rule setsum_set_distinct_conv_listsum) simp
 
 
 text {* Code for summation over ints. *}
 
-lemma greaterThanLessThan_upto [code unfold]:
+lemma greaterThanLessThan_upto [code_unfold]:
   "{i<..<j::int} = set [i+1..j - 1]"
 by auto
 
-lemma atLeastLessThan_upto [code unfold]:
+lemma atLeastLessThan_upto [code_unfold]:
   "{i..<j::int} = set [i..j - 1]"
 by auto
 
-lemma greaterThanAtMost_upto [code unfold]:
+lemma greaterThanAtMost_upto [code_unfold]:
   "{i<..j::int} = set [i+1..j]"
 by auto
 
-lemma atLeastAtMost_upto [code unfold]:
+lemma atLeastAtMost_upto [code_unfold]:
   "{i..j::int} = set [i..j]"
 by auto
 
-lemma setsum_set_upto_conv_listsum [code unfold]:
+lemma setsum_set_upto_conv_listsum [code_unfold]:
   "setsum f (set [i..j::int]) = listsum (map f [i..j])"
 by (rule setsum_set_distinct_conv_listsum) simp
 
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -467,7 +467,7 @@
 
 lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
 
-lemmas [code ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
+lemmas [code_ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
 
 code_module BV
 contains
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Nat.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -1200,9 +1200,9 @@
 text {* for code generation *}
 
 definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
-  funpow_code_def [code post]: "funpow = compow"
+  funpow_code_def [code_post]: "funpow = compow"
 
-lemmas [code unfold] = funpow_code_def [symmetric]
+lemmas [code_unfold] = funpow_code_def [symmetric]
 
 lemma [code]:
   "funpow 0 f = id"
@@ -1265,7 +1265,7 @@
 
 end
 
-declare of_nat_code [code, code unfold, code inline del]
+declare of_nat_code [code, code_unfold, code_inline del]
 
 text{*Class for unital semirings with characteristic zero.
  Includes non-ordered rings like the complex numbers.*}
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Nat_Numeral.thy
--- a/src/HOL/Nat_Numeral.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -20,13 +20,13 @@
 begin
 
 definition
-  nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)"
+  nat_number_of_def [code_inline, code del]: "number_of v = nat (number_of v)"
 
 instance ..
 
 end
 
-lemma [code post]:
+lemma [code_post]:
   "nat (number_of v) = number_of v"
   unfolding nat_number_of_def ..
 
@@ -316,13 +316,13 @@
 lemma nat_number_of [simp]: "nat (number_of w) = number_of w"
 by (simp add: nat_number_of_def)
 
-lemma nat_numeral_0_eq_0 [simp, code post]: "Numeral0 = (0::nat)"
+lemma nat_numeral_0_eq_0 [simp, code_post]: "Numeral0 = (0::nat)"
 by (simp add: nat_number_of_def)
 
 lemma nat_numeral_1_eq_1 [simp]: "Numeral1 = (1::nat)"
 by (simp add: nat_1 nat_number_of_def)
 
-lemma numeral_1_eq_Suc_0 [code post]: "Numeral1 = Suc 0"
+lemma numeral_1_eq_Suc_0 [code_post]: "Numeral1 = Suc 0"
 by (simp add: nat_numeral_1_eq_1)
 
 
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Option.thy
--- a/src/HOL/Option.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Option.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -94,7 +94,7 @@
 subsubsection {* Code generator setup *}
 
 definition is_none :: "'a option \<Rightarrow> bool" where
-  [code post]: "is_none x \<longleftrightarrow> x = None"
+  [code_post]: "is_none x \<longleftrightarrow> x = None"
 
 lemma is_none_code [code]:
   shows "is_none None \<longleftrightarrow> True"
@@ -105,7 +105,7 @@
   "is_none x \<longleftrightarrow> x = None"
   by (simp add: is_none_def)
 
-lemma [code inline]:
+lemma [code_inline]:
   "eq_class.eq x None \<longleftrightarrow> is_none x"
   by (simp add: eq is_none_none)
 
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Orderings.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -268,13 +268,13 @@
 
 text {* Explicit dictionaries for code generation *}
 
-lemma min_ord_min [code, code unfold, code inline del]:
+lemma min_ord_min [code, code_unfold, code_inline del]:
   "min = ord.min (op \<le>)"
   by (rule ext)+ (simp add: min_def ord.min_def)
 
 declare ord.min_def [code]
 
-lemma max_ord_max [code, code unfold, code inline del]:
+lemma max_ord_max [code, code_unfold, code_inline del]:
   "max = ord.max (op \<le>)"
   by (rule ext)+ (simp add: max_def ord.max_def)
 
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Power.thy
--- a/src/HOL/Power.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Power.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -455,7 +455,7 @@
 
 subsection {* Code generator tweak *}
 
-lemma power_power_power [code, code unfold, code inline del]:
+lemma power_power_power [code, code_unfold, code_inline del]:
   "power = power.power (1::'a::{power}) (op *)"
   unfolding power_def power.power_def ..
 
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Rational.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -93,10 +93,10 @@
 begin
 
 definition
-  Zero_rat_def [code, code unfold]: "0 = Fract 0 1"
+  Zero_rat_def [code, code_unfold]: "0 = Fract 0 1"
 
 definition
-  One_rat_def [code, code unfold]: "1 = Fract 1 1"
+  One_rat_def [code, code_unfold]: "1 = Fract 1 1"
 
 definition
   add_rat_def [code del]:
@@ -211,7 +211,7 @@
 
 end
 
-lemma rat_number_collapse [code post]:
+lemma rat_number_collapse [code_post]:
   "Fract 0 k = 0"
   "Fract 1 1 = 1"
   "Fract (number_of k) 1 = number_of k"
@@ -219,7 +219,7 @@
   by (cases "k = 0")
     (simp_all add: Zero_rat_def One_rat_def number_of_is_id number_of_eq of_int_rat eq_rat Fract_def)
 
-lemma rat_number_expand [code unfold]:
+lemma rat_number_expand [code_unfold]:
   "0 = Fract 0 1"
   "1 = Fract 1 1"
   "number_of k = Fract (number_of k) 1"
@@ -291,11 +291,11 @@
 lemma Fract_of_int_quotient: "Fract k l = of_int k / of_int l"
   by (simp add: Fract_of_int_eq [symmetric])
 
-lemma Fract_number_of_quotient [code post]:
+lemma Fract_number_of_quotient [code_post]:
   "Fract (number_of k) (number_of l) = number_of k / number_of l"
   unfolding Fract_of_int_quotient number_of_is_id number_of_eq ..
 
-lemma Fract_1_number_of [code post]:
+lemma Fract_1_number_of [code_post]:
   "Fract 1 (number_of k) = 1 / number_of k"
   unfolding Fract_of_int_quotient number_of_eq by simp
 
@@ -1003,7 +1003,7 @@
 
 definition (in term_syntax)
   valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
-  [code inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
+  [code_inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
 
 notation fcomp (infixl "o>" 60)
 notation scomp (infixl "o\<rightarrow>" 60)
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/RealDef.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -559,8 +559,8 @@
   real :: "'a => real"
 
 defs (overloaded)
-  real_of_nat_def [code unfold]: "real == real_of_nat"
-  real_of_int_def [code unfold]: "real == real_of_int"
+  real_of_nat_def [code_unfold]: "real == real_of_nat"
+  real_of_int_def [code_unfold]: "real == real_of_int"
 
 lemma real_eq_of_nat: "real = of_nat"
   unfolding real_of_nat_def ..
@@ -946,7 +946,7 @@
 
 end
 
-lemma [code unfold, symmetric, code post]:
+lemma [code_unfold, symmetric, code_post]:
   "number_of k = real_of_int (number_of k)"
   unfolding number_of_is_id real_number_of_def ..
 
@@ -1061,29 +1061,29 @@
 
 code_datatype Ratreal
 
-lemma Ratreal_number_collapse [code post]:
+lemma Ratreal_number_collapse [code_post]:
   "Ratreal 0 = 0"
   "Ratreal 1 = 1"
   "Ratreal (number_of k) = number_of k"
 by simp_all
 
-lemma zero_real_code [code, code unfold]:
+lemma zero_real_code [code, code_unfold]:
   "0 = Ratreal 0"
 by simp
 
-lemma one_real_code [code, code unfold]:
+lemma one_real_code [code, code_unfold]:
   "1 = Ratreal 1"
 by simp
 
-lemma number_of_real_code [code unfold]:
+lemma number_of_real_code [code_unfold]:
   "number_of k = Ratreal (number_of k)"
 by simp
 
-lemma Ratreal_number_of_quotient [code post]:
+lemma Ratreal_number_of_quotient [code_post]:
   "Ratreal (number_of r) / Ratreal (number_of s) = number_of r / number_of s"
 by simp
 
-lemma Ratreal_number_of_quotient2 [code post]:
+lemma Ratreal_number_of_quotient2 [code_post]:
   "Ratreal (number_of r / number_of s) = number_of r / number_of s"
 unfolding Ratreal_number_of_quotient [symmetric] Ratreal_def of_rat_divide ..
 
@@ -1129,7 +1129,7 @@
 
 definition (in term_syntax)
   valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
-  [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
+  [code_inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
 
 notation fcomp (infixl "o>" 60)
 notation scomp (infixl "o\<rightarrow>" 60)
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/SetInterval.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -284,8 +284,8 @@
 lemma atLeast0AtMost: "{0..n::nat} = {..n}"
 by(simp add:atMost_def atLeastAtMost_def)
 
-declare atLeast0LessThan[symmetric, code unfold]
-        atLeast0AtMost[symmetric, code unfold]
+declare atLeast0LessThan[symmetric, code_unfold]
+        atLeast0AtMost[symmetric, code_unfold]
 
 lemma atLeastLessThan0: "{m..<0::nat} = {}"
 by (simp add: atLeastLessThan_def)
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/String.thy
--- a/src/HOL/String.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/String.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -58,11 +58,11 @@
 end
 *}
 
-lemma char_case_nibble_pair [code, 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, 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 1d93369079c4 -r fafefd0b341c src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Tue Jul 14 10:56:43 2009 +0200
@@ -697,7 +697,8 @@
 
 val setup =
   add_codegen "inductive" inductive_codegen #>
-  Code.add_attribute ("ind", Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
-    Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add);
+  Attrib.setup @{binding code_ind} (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) --
+    Scan.option (Args.$$$ "params" |-- Args.colon |-- OuterParse.nat) >> uncurry add))
+    "introduction rules for executable predicates";
 
 end;
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Tue Jul 14 10:56:43 2009 +0200
@@ -541,8 +541,9 @@
     "declare rules for converting between predicate and set notation" #>
   Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att) "convert rule to set notation" #>
   Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att) "convert rule to predicate notation" #>
-  Code.add_attribute ("ind_set",
-    Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att) #>
+  Attrib.setup @{binding code_ind_set}
+    (Scan.lift (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att))
+    "introduction rules for executable predicates" #>
   Codegen.add_preprocessor codegen_preproc #>
   Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
     "declaration of monotonicity rule for set operators" #>
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Tue Jul 14 10:56:43 2009 +0200
@@ -23,15 +23,13 @@
   fun merge _ = Symtab.merge (K true);
 );
 
-fun add_thm NONE thm thy = Code.add_eqn thm thy
-  | add_thm (SOME module_name) thm thy =
-      let
-        val (thm', _) = Code.mk_eqn thy (thm, true)
-      in
-        thy
-        |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
-        |> Code.add_eqn thm'
-      end;
+fun add_thm_target module_name thm thy =
+  let
+    val (thm', _) = Code.mk_eqn thy (thm, true)
+  in
+    thy
+    |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
+  end;
 
 fun expand_eta thy [] = []
   | expand_eta thy (thms as thm :: _) =
@@ -163,15 +161,8 @@
         end)
   | _ => NONE);
 
-val setup = let
-  fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
-    (add_thm opt_module thm) I);
-  val del = Thm.declaration_attribute (fn thm => Context.mapping
-    (Code.del_eqn thm) I);
-in
+val setup = 
   add_codegen "recfun" recfun_codegen
-  #> Code.add_attribute ("", Args.del |-- Scan.succeed del
-     || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)
-end;
+  #> Code.set_code_target_attr add_thm_target;
 
 end;
diff -r 1d93369079c4 -r fafefd0b341c src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/HOL/ex/Numeral.thy	Tue Jul 14 10:56:43 2009 +0200
@@ -751,14 +751,14 @@
 subsection {* Code generator setup for @{typ int} *}
 
 definition Pls :: "num \<Rightarrow> int" where
-  [simp, code post]: "Pls n = of_num n"
+  [simp, code_post]: "Pls n = of_num n"
 
 definition Mns :: "num \<Rightarrow> int" where
-  [simp, code post]: "Mns n = - of_num n"
+  [simp, code_post]: "Mns n = - of_num n"
 
 code_datatype "0::int" Pls Mns
 
-lemmas [code inline] = Pls_def [symmetric] Mns_def [symmetric]
+lemmas [code_inline] = Pls_def [symmetric] Mns_def [symmetric]
 
 definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
   [simp, code del]: "sub m n = (of_num m - of_num n)"
@@ -874,10 +874,10 @@
   using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
   by (simp_all add: of_num_less_iff)
 
-lemma [code inline del]: "(0::int) \<equiv> Numeral0" by simp
-lemma [code inline del]: "(1::int) \<equiv> Numeral1" by simp
-declare zero_is_num_zero [code inline del]
-declare one_is_num_one [code inline del]
+lemma [code_inline del]: "(0::int) \<equiv> Numeral0" by simp
+lemma [code_inline del]: "(1::int) \<equiv> Numeral1" by simp
+declare zero_is_num_zero [code_inline del]
+declare one_is_num_one [code_inline del]
 
 hide (open) const sub dup
 
diff -r 1d93369079c4 -r fafefd0b341c src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/Pure/Isar/code.ML	Tue Jul 14 10:56:43 2009 +0200
@@ -62,7 +62,7 @@
   val print_codesetup: theory -> unit
 
   (*infrastructure*)
-  val add_attribute: string * attribute parser -> theory -> theory
+  val set_code_target_attr: (string -> thm -> theory -> theory) -> theory -> theory
   val purge_data: theory -> theory
 end;
 
@@ -235,31 +235,6 @@
   end;
 
 
-(** code attributes **)
-
-structure Code_Attr = TheoryDataFun (
-  type T = (string * attribute parser) list;
-  val empty = [];
-  val copy = I;
-  val extend = I;
-  fun merge _ = AList.merge (op = : string * string -> bool) (K true);
-);
-
-fun add_attribute (attr as (name, _)) =
-  let
-    fun add_parser ("", parser) attrs = attrs |> rev |> AList.update (op =) ("", parser) |> rev
-      | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs;
-  in Code_Attr.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 _ = Context.>> (Context.map_theory
-  (Attrib.setup (Binding.name "code")
-    (Scan.peek (fn context =>
-      List.foldr op || Scan.fail (map snd (Code_Attr.get (Context.theory_of context)))))
-    "declare theorems for code generation"));
-
-
 (** data store **)
 
 (* code equations *)
@@ -543,7 +518,7 @@
       in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
     fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
       let
-        val _ = if tyco' <> tyco
+        val _ = if (tyco' : string) <> tyco
           then error "Different type constructors in constructor set"
           else ();
         val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
@@ -911,18 +886,32 @@
  of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
   | NONE => thy;
 
+structure Code_Attr = TheoryDataFun (
+  type T = (string -> thm -> theory -> theory) option;
+  val empty = NONE;
+  val copy = I;
+  val extend = I;
+  fun merge _ (NONE, f2) = f2
+    | merge _ (f1, _) = f1;
+);
+
+fun set_code_target_attr f = Code_Attr.map (K (SOME f));
+
 val _ = Context.>> (Context.map_theory
   (let
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
-    fun add_simple_attribute (name, f) =
-      add_attribute (name, Scan.succeed (mk_attribute f));
-    fun add_del_attribute (name, (add, del)) =
-      add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
-        || Scan.succeed (mk_attribute add))
+    val code_attribute_parser =
+      Args.del |-- Scan.succeed (mk_attribute del_eqn)
+      || Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
+      || (Args.$$$ "target" |-- Args.colon |-- Args.name >>
+           (fn prefix => mk_attribute (fn thm => fn thy => thy
+             |> add_warning_eqn thm
+             |> the_default ((K o K) I) (Code_Attr.get thy) prefix thm)))
+      || Scan.succeed (mk_attribute add_warning_eqn);
   in
     Type_Interpretation.init
-    #> add_del_attribute ("", (add_warning_eqn, del_eqn))
-    #> add_simple_attribute ("nbe", add_nbe_eqn)
+    #> Attrib.setup (Binding.name "code") (Scan.lift code_attribute_parser)
+        "declare theorems for code generation"
   end));
 
 
diff -r 1d93369079c4 -r fafefd0b341c src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Mon Jul 13 19:07:05 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML	Tue Jul 14 10:56:43 2009 +0200
@@ -526,14 +526,16 @@
 val setup = 
   let
     fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
-    fun add_del_attribute (name, (add, del)) =
-      Code.add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
-        || Scan.succeed (mk_attribute add))
+    fun add_del_attribute_parser (add, del) =
+      Attrib.add_del (mk_attribute add) (mk_attribute del);
   in
-    add_del_attribute ("inline", (add_inline, del_inline))
-    #> add_del_attribute ("post", (add_post, del_post))
-    #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
-       (fn thm => Context.mapping (Codegen.add_unfold thm #> add_inline thm) I)))
+    Attrib.setup @{binding code_inline} (add_del_attribute_parser (add_inline, del_inline))
+        "preprocessing equations for code generator"
+    #> Attrib.setup @{binding code_post} (add_del_attribute_parser (add_post, del_post))
+        "postprocessing equations for code generator"
+    #> Attrib.setup @{binding code_unfold} (Scan.succeed (mk_attribute
+       (fn thm => Codegen.add_unfold thm #> add_inline thm)))
+        "preprocessing equations for code generators"
   end;
 
 val _ =