# HG changeset patch
# User haftmann
# Date 1285148788 -7200
# Node ID e5448cf9a04885a3b5ab7f416b70fabf98b7e3b1
# Parent  ae2c3059f8cc05ccbe98f850014c9b4814bf4112# Parent  23bdf736d84f83747693c7db0f5fec23643f55b3
merged

diff -r ae2c3059f8cc -r e5448cf9a048 doc-src/Codegen/IsaMakefile
--- a/doc-src/Codegen/IsaMakefile	Wed Sep 22 10:02:39 2010 +0200
+++ b/doc-src/Codegen/IsaMakefile	Wed Sep 22 11:46:28 2010 +0200
@@ -26,7 +26,7 @@
 $(THY): Thy/ROOT.ML Thy/*.thy ../antiquote_setup.ML ../more_antiquote.ML
 	@$(USEDIR) -m no_brackets -m iff HOL-Library Thy
 	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
-	 Thy/document/pdfsetup.sty Thy/document/session.tex
+	  Thy/document/pdfsetup.sty Thy/document/session.tex
 
 
 ## clean
diff -r ae2c3059f8cc -r e5448cf9a048 doc-src/Codegen/Thy/Evaluation.thy
--- a/doc-src/Codegen/Thy/Evaluation.thy	Wed Sep 22 10:02:39 2010 +0200
+++ b/doc-src/Codegen/Thy/Evaluation.thy	Wed Sep 22 11:46:28 2010 +0200
@@ -70,9 +70,9 @@
   Evaluation is carried out in a target language \emph{Eval} which
   inherits from \emph{SML} but for convenience uses parts of the
   Isabelle runtime environment.  The soundness of computation carried
-  out there crucially on the correctness of the code generator; this
-  is one of the reasons why you should not use adaptation (see
-  \secref{sec:adaptation}) frivolously.
+  out there depends crucially on the correctness of the code
+  generator; this is one of the reasons why you should not use
+  adaptation (see \secref{sec:adaptation}) frivolously.
 *}
 
 
@@ -187,19 +187,19 @@
 
 subsection {* Intimate connection between logic and system runtime *}
 
-text {* FIXME *}
+text {*
+  The toolbox of static evaluation conversions forms a reasonable base
+  to interweave generated code and system tools.  However in some
+  situations more direct interaction is desirable.
+*}
 
 
-subsubsection {* Static embedding of generated code into system runtime -- the code antiquotation *}
+subsubsection {* Static embedding of generated code into system runtime -- the @{text code} antiquotation *}
 
 text {*
-  FIXME
-
-  In scenarios involving techniques like reflection it is quite common
-  that code generated from a theory forms the basis for implementing a
-  proof procedure in @{text SML}.  To facilitate interfacing of
-  generated code with system code, the code generator provides a
-  @{text code} antiquotation:
+  The @{text code} antiquotation allows to include constants from
+  generated code directly into ML system code, as in the following toy
+  example:
 *}
 
 datatype %quote form = T | F | And form form | Or form form (*<*)
@@ -214,23 +214,66 @@
 *}
 
 text {*
-  \noindent @{text code} takes as argument the name of a constant;  after the
-  whole @{text SML} is read, the necessary code is generated transparently
-  and the corresponding constant names are inserted.  This technique also
-  allows to use pattern matching on constructors stemming from compiled
-  @{text "datatypes"}.
+  \noindent @{text code} takes as argument the name of a constant;
+  after the whole ML is read, the necessary code is generated
+  transparently and the corresponding constant names are inserted.
+  This technique also allows to use pattern matching on constructors
+  stemming from compiled @{text "datatypes"}.  Note that it is not
+  possible to refer to constants which carry adaptations by means of
+  @{text code}; here you have to refer to the adapted code directly.
 
-  For a less simplistic example, theory @{text Ferrack} is
-  a good reference.
+  For a less simplistic example, theory @{text Approximation} in
+  the @{text Decision_Procs} session is a good reference.
 *}
 
 
 subsubsection {* Static embedding of generated code into system runtime -- @{text code_reflect} *}
 
-text {* FIXME @{command_def code_reflect} *}
+text {*
+  The @{text code} antiquoation is lightweight, but the generated code
+  is only accessible while the ML section is processed.  Sometimes this
+  is not appropriate, especially if the generated code contains datatype
+  declarations which are shared with other parts of the system.  In these
+  cases, @{command_def code_reflect} can be used:
+*}
+
+code_reflect %quote Sum_Type
+  datatypes sum = Inl | Inr
+  functions "Sum_Type.Projl" "Sum_Type.Projr"
+
+text {*
+  \noindent @{command_def code_reflect} takes a structure name and
+  references to datatypes and functions; for these code is compiled
+  into the named ML structure and the \emph{Eval} target is modified
+  in a way that future code generation will reference these
+  precompiled versions of the given datatypes and functions.  This
+  also allows to refer to the referenced datatypes and functions from
+  arbitrary ML code as well.
+
+  A typical example for @{command code_reflect} can be found in the
+  @{theory Predicate} theory.
+*}
+
 
 subsubsection {* Separate compilation -- @{text code_reflect} *}
 
-text {* FIXME *}
+text {*
+  For technical reasons it is sometimes necessary to separate
+  generation and compilation of code which is supposed to be used in
+  the system runtime.  For this @{command code_reflect} with an
+  optional @{text "file"} argument can be used:
+*}
+
+code_reflect %quote Rat
+  datatypes rat = Frct
+  functions Fract
+    "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
+    "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
+  file "examples/rat.ML"
+
+text {*
+  \noindent This just generates the references code to the specified
+  file which can be included into the system runtime later on.
+*}
 
 end
diff -r ae2c3059f8cc -r e5448cf9a048 doc-src/Codegen/Thy/document/Evaluation.tex
--- a/doc-src/Codegen/Thy/document/Evaluation.tex	Wed Sep 22 10:02:39 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Evaluation.tex	Wed Sep 22 11:46:28 2010 +0200
@@ -96,9 +96,9 @@
   Evaluation is carried out in a target language \emph{Eval} which
   inherits from \emph{SML} but for convenience uses parts of the
   Isabelle runtime environment.  The soundness of computation carried
-  out there crucially on the correctness of the code generator; this
-  is one of the reasons why you should not use adaptation (see
-  \secref{sec:adaptation}) frivolously.%
+  out there depends crucially on the correctness of the code
+  generator; this is one of the reasons why you should not use
+  adaptation (see \secref{sec:adaptation}) frivolously.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -242,22 +242,20 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME%
+The toolbox of static evaluation conversions forms a reasonable base
+  to interweave generated code and system tools.  However in some
+  situations more direct interaction is desirable.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsubsection{Static embedding of generated code into system runtime -- the code antiquotation%
+\isamarkupsubsubsection{Static embedding of generated code into system runtime -- the \isa{code} antiquotation%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME
-
-  In scenarios involving techniques like reflection it is quite common
-  that code generated from a theory forms the basis for implementing a
-  proof procedure in \isa{SML}.  To facilitate interfacing of
-  generated code with system code, the code generator provides a
-  \isa{code} antiquotation:%
+The \isa{code} antiquotation allows to include constants from
+  generated code directly into ML system code, as in the following toy
+  example:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -313,14 +311,16 @@
 \endisadelimquotett
 %
 \begin{isamarkuptext}%
-\noindent \isa{code} takes as argument the name of a constant;  after the
-  whole \isa{SML} is read, the necessary code is generated transparently
-  and the corresponding constant names are inserted.  This technique also
-  allows to use pattern matching on constructors stemming from compiled
-  \isa{datatypes}.
+\noindent \isa{code} takes as argument the name of a constant;
+  after the whole ML is read, the necessary code is generated
+  transparently and the corresponding constant names are inserted.
+  This technique also allows to use pattern matching on constructors
+  stemming from compiled \isa{datatypes}.  Note that it is not
+  possible to refer to constants which carry adaptations by means of
+  \isa{code}; here you have to refer to the adapted code directly.
 
-  For a less simplistic example, theory \isa{Ferrack} is
-  a good reference.%
+  For a less simplistic example, theory \isa{Approximation} in
+  the \isa{Decision{\isacharunderscore}Procs} session is a good reference.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -329,7 +329,41 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME \indexdef{}{command}{code\_reflect}\hypertarget{command.code-reflect}{\hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}}%
+The \isa{code} antiquoation is lightweight, but the generated code
+  is only accessible while the ML section is processed.  Sometimes this
+  is not appropriate, especially if the generated code contains datatype
+  declarations which are shared with other parts of the system.  In these
+  cases, \indexdef{}{command}{code\_reflect}\hypertarget{command.code-reflect}{\hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}} can be used:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}reflect}\isamarkupfalse%
+\ Sum{\isacharunderscore}Type\isanewline
+\ \ \isakeyword{datatypes}\ sum\ {\isacharequal}\ Inl\ {\isacharbar}\ Inr\isanewline
+\ \ \isakeyword{functions}\ {\isachardoublequoteopen}Sum{\isacharunderscore}Type{\isachardot}Projl{\isachardoublequoteclose}\ {\isachardoublequoteopen}Sum{\isacharunderscore}Type{\isachardot}Projr{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent \indexdef{}{command}{code\_reflect}\hypertarget{command.code-reflect}{\hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}} takes a structure name and
+  references to datatypes and functions; for these code is compiled
+  into the named ML structure and the \emph{Eval} target is modified
+  in a way that future code generation will reference these
+  precompiled versions of the given datatypes and functions.  This
+  also allows to refer to the referenced datatypes and functions from
+  arbitrary ML code as well.
+
+  A typical example for \hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}} can be found in the
+  \hyperlink{theory.Predicate}{\mbox{\isa{Predicate}}} theory.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -338,7 +372,35 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME%
+For technical reasons it is sometimes necessary to separate
+  generation and compilation of code which is supposed to be used in
+  the system runtime.  For this \hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}} with an
+  optional \isa{file} argument can be used:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\isatagquote
+\isacommand{code{\isacharunderscore}reflect}\isamarkupfalse%
+\ Rat\isanewline
+\ \ \isakeyword{datatypes}\ rat\ {\isacharequal}\ Frct\isanewline
+\ \ \isakeyword{functions}\ Fract\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}plus\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}minus\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}times\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharparenleft}divide\ {\isacharcolon}{\isacharcolon}\ rat\ {\isasymRightarrow}\ rat\ {\isasymRightarrow}\ rat{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \isakeyword{file}\ {\isachardoublequoteopen}examples{\isacharslash}rat{\isachardot}ML{\isachardoublequoteclose}%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
+%
+\begin{isamarkuptext}%
+\noindent This just generates the references code to the specified
+  file which can be included into the system runtime later on.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r ae2c3059f8cc -r e5448cf9a048 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Sep 22 10:02:39 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Sep 22 11:46:28 2010 +0200
@@ -996,6 +996,7 @@
     @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"}
   \end{matharray}
 
   \begin{rail}
@@ -1068,6 +1069,10 @@
     'code\_modulename' target ( ( string string ) + )
     ;
 
+    'code\_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
+      ( 'functions' ( string + ) ) ? ( 'file' string ) ?
+    ;
+
     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     ;
 
@@ -1076,8 +1081,9 @@
   \begin{description}
 
   \item @{command (HOL) "export_code"} generates code for a given list
-  of constants in the specified target language(s).  If no serialization
-  instruction is given, only abstract code is generated internally.
+  of constants in the specified target language(s).  If no
+  serialization instruction is given, only abstract code is generated
+  internally.
 
   Constants may be specified by giving them literally, referring to
   all executable contants within a certain theory by giving @{text
@@ -1089,20 +1095,20 @@
   after the @{keyword "module_name"} keyword; then \emph{all} code is
   placed in this module.
 
-  For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification refers to a
-  single file; for \emph{Haskell}, it refers to a whole directory,
-  where code is generated in multiple files reflecting the module
-  hierarchy.  Omitting the file specification denotes standard
+  For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification
+  refers to a single file; for \emph{Haskell}, it refers to a whole
+  directory, where code is generated in multiple files reflecting the
+  module hierarchy.  Omitting the file specification denotes standard
   output.
 
   Serializers take an optional list of arguments in parentheses.  For
   \emph{SML} and \emph{OCaml}, ``@{text no_signatures}`` omits
   explicit module signatures.
   
-  For \emph{Haskell} a module name prefix may be given using the ``@{text
-  "root:"}'' argument; ``@{text string_classes}'' adds a ``@{verbatim
-  "deriving (Read, Show)"}'' clause to each appropriate datatype
-  declaration.
+  For \emph{Haskell} a module name prefix may be given using the
+  ``@{text "root:"}'' argument; ``@{text string_classes}'' adds a
+  ``@{verbatim "deriving (Read, Show)"}'' clause to each appropriate
+  datatype declaration.
 
   \item @{attribute (HOL) code} explicitly selects (or with option
   ``@{text "del"}'' deselects) a code equation for code generation.
@@ -1112,8 +1118,8 @@
   code equations on abstract datatype representations respectively.
 
   \item @{command (HOL) "code_abort"} declares constants which are not
-  required to have a definition by means of code equations; if
-  needed these are implemented by program abort instead.
+  required to have a definition by means of code equations; if needed
+  these are implemented by program abort instead.
 
   \item @{command (HOL) "code_datatype"} specifies a constructor set
   for a logical type.
@@ -1121,17 +1127,16 @@
   \item @{command (HOL) "print_codesetup"} gives an overview on
   selected code equations and code generator datatypes.
 
-  \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_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 @{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_codeproc"} prints the setup
-  of the code generator preprocessor.
+  \item @{command (HOL) "print_codeproc"} prints the setup of the code
+  generator preprocessor.
 
   \item @{command (HOL) "code_thms"} prints a list of theorems
   representing the corresponding program containing all given
@@ -1173,11 +1178,21 @@
   \item @{command (HOL) "code_modulename"} declares aliasings from one
   module name onto another.
 
+  \item @{command (HOL) "code_reflect"} without a ``@{text "file"}''
+  argument compiles code into the system runtime environment and
+  modifies the code generator setup that future invocations of system
+  runtime code generation referring to one of the ``@{text
+  "datatypes"}'' or ``@{text "functions"}'' entities use these precompiled
+  entities.  With a ``@{text "file"}'' argument, the corresponding code
+  is generated into that specified file without modifying the code
+  generator setup.
+
   \end{description}
 
-  The other framework generates code from both functional and relational
-  programs to SML.  See \cite{isabelle-HOL} for further information
-  (this actually covers the new-style theory format as well).
+  The other framework generates code from both functional and
+  relational programs to SML.  See \cite{isabelle-HOL} for further
+  information (this actually covers the new-style theory format as
+  well).
 
   \begin{matharray}{rcl}
     @{command_def (HOL) "code_module"} & : & @{text "theory \<rightarrow> theory"} \\
diff -r ae2c3059f8cc -r e5448cf9a048 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Sep 22 10:02:39 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Sep 22 11:46:28 2010 +0200
@@ -1012,6 +1012,7 @@
     \indexdef{HOL}{command}{code\_monad}\hypertarget{command.HOL.code-monad}{\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     \indexdef{HOL}{command}{code\_include}\hypertarget{command.HOL.code-include}{\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+    \indexdef{HOL}{command}{code\_reflect}\hypertarget{command.HOL.code-reflect}{\hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}}
   \end{matharray}
 
   \begin{rail}
@@ -1084,6 +1085,10 @@
     'code\_modulename' target ( ( string string ) + )
     ;
 
+    'code\_reflect' string ( 'datatypes' ( string '=' ( string + '|' ) + 'and' ) ) ? \\
+      ( 'functions' ( string + ) ) ? ( 'file' string ) ?
+    ;
+
     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     ;
 
@@ -1092,8 +1097,9 @@
   \begin{description}
 
   \item \hyperlink{command.HOL.export-code}{\mbox{\isa{\isacommand{export{\isacharunderscore}code}}}} generates code for a given list
-  of constants in the specified target language(s).  If no serialization
-  instruction is given, only abstract code is generated internally.
+  of constants in the specified target language(s).  If no
+  serialization instruction is given, only abstract code is generated
+  internally.
 
   Constants may be specified by giving them literally, referring to
   all executable contants within a certain theory by giving \isa{{\isachardoublequote}name{\isachardot}{\isacharasterisk}{\isachardoublequote}}, or referring to \emph{all} executable constants currently
@@ -1104,18 +1110,20 @@
   after the \hyperlink{keyword.module-name}{\mbox{\isa{\isakeyword{module{\isacharunderscore}name}}}} keyword; then \emph{all} code is
   placed in this module.
 
-  For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification refers to a
-  single file; for \emph{Haskell}, it refers to a whole directory,
-  where code is generated in multiple files reflecting the module
-  hierarchy.  Omitting the file specification denotes standard
+  For \emph{SML}, \emph{OCaml} and \emph{Scala} the file specification
+  refers to a single file; for \emph{Haskell}, it refers to a whole
+  directory, where code is generated in multiple files reflecting the
+  module hierarchy.  Omitting the file specification denotes standard
   output.
 
   Serializers take an optional list of arguments in parentheses.  For
   \emph{SML} and \emph{OCaml}, ``\isa{no{\isacharunderscore}signatures}`` omits
   explicit module signatures.
   
-  For \emph{Haskell} a module name prefix may be given using the ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a ``\verb|deriving (Read, Show)|'' clause to each appropriate datatype
-  declaration.
+  For \emph{Haskell} a module name prefix may be given using the
+  ``\isa{{\isachardoublequote}root{\isacharcolon}{\isachardoublequote}}'' argument; ``\isa{string{\isacharunderscore}classes}'' adds a
+  ``\verb|deriving (Read, Show)|'' clause to each appropriate
+  datatype declaration.
 
   \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
   ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code generation.
@@ -1125,8 +1133,8 @@
   code equations on abstract datatype representations respectively.
 
   \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
-  required to have a definition by means of code equations; if
-  needed these are implemented by program abort instead.
+  required to have a definition by means of code equations; if needed
+  these are implemented by program abort instead.
 
   \item \hyperlink{command.HOL.code-datatype}{\mbox{\isa{\isacommand{code{\isacharunderscore}datatype}}}} specifies a constructor set
   for a logical type.
@@ -1134,17 +1142,15 @@
   \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
   selected code equations and code generator datatypes.
 
-  \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-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{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-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup
-  of the code generator preprocessor.
+  \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup of the code
+  generator preprocessor.
 
   \item \hyperlink{command.HOL.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} prints a list of theorems
   representing the corresponding program containing all given
@@ -1186,11 +1192,20 @@
   \item \hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}} declares aliasings from one
   module name onto another.
 
+  \item \hyperlink{command.HOL.code-reflect}{\mbox{\isa{\isacommand{code{\isacharunderscore}reflect}}}} without a ``\isa{{\isachardoublequote}file{\isachardoublequote}}''
+  argument compiles code into the system runtime environment and
+  modifies the code generator setup that future invocations of system
+  runtime code generation referring to one of the ``\isa{{\isachardoublequote}datatypes{\isachardoublequote}}'' or ``\isa{{\isachardoublequote}functions{\isachardoublequote}}'' entities use these precompiled
+  entities.  With a ``\isa{{\isachardoublequote}file{\isachardoublequote}}'' argument, the corresponding code
+  is generated into that specified file without modifying the code
+  generator setup.
+
   \end{description}
 
-  The other framework generates code from both functional and relational
-  programs to SML.  See \cite{isabelle-HOL} for further information
-  (this actually covers the new-style theory format as well).
+  The other framework generates code from both functional and
+  relational programs to SML.  See \cite{isabelle-HOL} for further
+  information (this actually covers the new-style theory format as
+  well).
 
   \begin{matharray}{rcl}
     \indexdef{HOL}{command}{code\_module}\hypertarget{command.HOL.code-module}{\hyperlink{command.HOL.code-module}{\mbox{\isa{\isacommand{code{\isacharunderscore}module}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
diff -r ae2c3059f8cc -r e5448cf9a048 src/HOL/Imperative_HOL/Overview.thy
--- a/src/HOL/Imperative_HOL/Overview.thy	Wed Sep 22 10:02:39 2010 +0200
+++ b/src/HOL/Imperative_HOL/Overview.thy	Wed Sep 22 11:46:28 2010 +0200
@@ -61,7 +61,7 @@
   fact collection @{text execute_simps} contains appropriate rewrites
   for all fundamental operations.
 
-  Primitive fine-granular control over heaps is avialable through rule
+  Primitive fine-granular control over heaps is available through rule
   @{text Heap_cases}:
 
   \begin{quote}
@@ -231,13 +231,13 @@
       
     \item Whether one should prefer equational reasoning (fact
       collection @{text execute_simps} or relational reasoning (fact
-      collections @{text crel_intros} and @{text crel_elims}) dependes
-      on the problems.  For complex expressions or expressions
-      involving binders, the relation style usually is superior but
-      requires more proof text.
+      collections @{text crel_intros} and @{text crel_elims}) depends
+      on the problems to solve.  For complex expressions or
+      expressions involving binders, the relation style usually is
+      superior but requires more proof text.
 
     \item Note that you can extend the fact collections of Imperative
-      HOL yourself.
+      HOL yourself whenever appropriate.
 
   \end{itemize}
 *}
diff -r ae2c3059f8cc -r e5448cf9a048 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Wed Sep 22 10:02:39 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Wed Sep 22 11:46:28 2010 +0200
@@ -273,15 +273,17 @@
   by (simp add: ref'_def)
 
 
-text {* SML *}
+text {* SML / Eval *}
 
-code_type ref (SML "_/ Unsynchronized.ref")
+code_type ref (SML "_/ ref")
+code_type ref (Eval "_/ Unsynchronized.ref")
 code_const Ref (SML "raise/ (Fail/ \"bare Ref\")")
-code_const ref' (SML "(fn/ ()/ =>/ Unsynchronized.ref/ _)")
+code_const ref' (SML "(fn/ ()/ =>/ ref/ _)")
+code_const ref' (Eval "(fn/ ()/ =>/ Unsynchronized.ref/ _)")
 code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)")
 code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)")
 
-code_reserved SML Unsynchronized
+code_reserved Eval Unsynchronized
 
 
 text {* OCaml *}
diff -r ae2c3059f8cc -r e5448cf9a048 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Wed Sep 22 10:02:39 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Wed Sep 22 11:46:28 2010 +0200
@@ -106,6 +106,22 @@
 
 (* post- and preprocessing *)
 
+fun no_variables_conv conv ct =
+  let
+    val cert = Thm.cterm_of (Thm.theory_of_cterm ct);
+    val all_vars = fold_aterms (fn t as Free _ => insert (op aconvc) (cert t)
+      | t as Var _ => insert (op aconvc) (cert t)
+      | _ => I) (Thm.term_of ct) [];
+    fun apply_beta var thm = Thm.combination thm (Thm.reflexive var)
+      |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
+      |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
+  in
+    ct
+    |> fold_rev Thm.cabs all_vars
+    |> conv
+    |> fold apply_beta all_vars
+  end;
+
 fun trans_conv_rule conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
 
 fun eqn_conv conv ct =
@@ -141,7 +157,6 @@
 fun preprocess_conv thy ct =
   let
     val ctxt = ProofContext.init_global thy;
-    val _ = (Sign.no_frees ctxt o map_types (K dummyT) o Sign.no_vars ctxt) (Thm.term_of ct);
     val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
   in
     ct
@@ -149,7 +164,13 @@
     |> trans_conv_rule (AxClass.unoverload_conv thy)
   end;
 
-fun preprocess_term thy = term_of_conv thy (preprocess_conv thy);
+fun preprocess_term thy t =
+  let
+    val all_vars = fold_aterms (fn t as Free _ => insert (op aconv) t
+      | t as Var _ => insert (op aconv) t
+      | _ => I) t [];
+    val resubst = curry (Term.betapplys o swap) all_vars;
+  in (resubst, term_of_conv thy (preprocess_conv thy) (fold_rev lambda all_vars t)) end;
 
 fun postprocess_conv thy ct =
   let
@@ -198,8 +219,11 @@
 type code_algebra = (sort -> sort) * Sorts.algebra;
 type code_graph = ((string * sort) list * Code.cert) Graph.T;
 
-fun cert eqngr = snd o Graph.get_node eqngr;
-fun sortargs eqngr = map snd o fst o Graph.get_node eqngr;
+fun get_node eqngr const = Graph.get_node eqngr const
+  handle Graph.UNDEF _ => error ("No such constant in code equation graph: " ^ quote const);
+
+fun cert eqngr = snd o get_node eqngr;
+fun sortargs eqngr = map snd o fst o get_node eqngr;
 fun all eqngr = Graph.keys eqngr;
 
 fun pretty thy eqngr =
@@ -433,7 +457,7 @@
 
 fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
 
-fun dynamic_eval_conv thy conv ct =
+fun dynamic_eval_conv thy conv = no_variables_conv (fn ct =>
   let
     val thm1 = preprocess_conv thy ct;
     val ct' = Thm.rhs_of thm1;
@@ -447,11 +471,11 @@
     Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
       error ("could not construct evaluation proof:\n"
       ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
-  end;
+  end);
 
 fun dynamic_eval_value thy postproc evaluator t =
   let
-    val t' = preprocess_term thy t;
+    val (resubst, t') = preprocess_term thy t;
     val vs' = Term.add_tfrees t' [];
     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
@@ -459,7 +483,7 @@
     val result = evaluator algebra' eqngr' vs' t';
   in
     evaluator algebra' eqngr' vs' t'
-    |> postproc (postprocess_term thy)
+    |> postproc (postprocess_term thy o resubst)
   end;
 
 fun static_eval_conv thy consts conv =
@@ -467,9 +491,9 @@
     val (algebra, eqngr) = obtain true thy consts [];
     val conv' = conv algebra eqngr;
   in
-    Conv.tap_thy (fn thy => (preprocess_conv thy)
+    no_variables_conv (Conv.tap_thy (fn thy => (preprocess_conv thy)
       then_conv (fn ct => uncurry (conv' thy) (dest_cterm ct) ct)
-      then_conv (postprocess_conv thy))
+      then_conv (postprocess_conv thy)))
   end;
 
 fun static_eval_value thy postproc consts evaluator =
@@ -479,8 +503,9 @@
   in fn t =>
     t
     |> preprocess_term thy
-    |> (fn t => evaluator' thy (Term.add_tfrees t [])  t)
-    |> postproc (postprocess_term thy)
+    |-> (fn resubst => fn t => t
+    |> evaluator' thy (Term.add_tfrees t [])
+    |> postproc (postprocess_term thy o resubst))
   end;
 
 
diff -r ae2c3059f8cc -r e5448cf9a048 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Wed Sep 22 10:02:39 2010 +0200
+++ b/src/Tools/Code/code_runtime.ML	Wed Sep 22 11:46:28 2010 +0200
@@ -60,6 +60,11 @@
 
 type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
 
+fun reject_vars thy t =
+  let
+    val ctxt = ProofContext.init_global thy;
+  in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
+
 fun obtain_serializer thy some_target = Code_Target.produce_code_for thy
   (the_default target some_target) NONE "Code" [];
 
@@ -88,6 +93,7 @@
 
 fun dynamic_value_exn cookie thy some_target postproc t args =
   let
+    val _ = reject_vars thy t;
     fun evaluator naming program ((_, vs_ty), t) deps =
       base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args;
   in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end;
@@ -103,7 +109,7 @@
     val serializer = obtain_serializer thy some_target;
     fun evaluator naming program thy ((_, vs_ty), t) deps =
       base_evaluator cookie serializer naming thy program (vs_ty, t) deps [];
-  in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator end;
+  in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end;
 
 fun static_value_strict cookie thy some_target postproc consts t =
   Exn.release (static_value_exn cookie thy some_target postproc consts t);
@@ -121,6 +127,8 @@
 val put_truth = Truth_Result.put;
 val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");
 
+val reject_vars = fn thy => tap (reject_vars thy o Thm.term_of);
+
 fun check_holds serializer naming thy program vs_t deps ct =
   let
     val t = Thm.term_of ct;
@@ -143,7 +151,8 @@
   raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct);
 
 val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy
-  (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy));
+  (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy)
+  o reject_vars thy);
 
 fun static_holds_conv thy consts =
   let
@@ -151,6 +160,7 @@
   in
     Code_Thingol.static_eval_conv thy consts
       (fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program)
+    o reject_vars thy
   end;
 
 
diff -r ae2c3059f8cc -r e5448cf9a048 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Wed Sep 22 10:02:39 2010 +0200
+++ b/src/Tools/Code/code_simp.ML	Wed Sep 22 11:46:28 2010 +0200
@@ -6,7 +6,6 @@
 
 signature CODE_SIMP =
 sig
-  val no_frees_conv: conv -> conv
   val map_ss: (simpset -> simpset) -> theory -> theory
   val dynamic_eval_conv: conv
   val dynamic_eval_tac: theory -> int -> tactic
@@ -19,22 +18,6 @@
 structure Code_Simp : CODE_SIMP =
 struct
 
-(* avoid free variables during conversion *)
-
-fun no_frees_conv conv ct =
-  let
-    val frees = Thm.add_cterm_frees ct [];
-    fun apply_beta free thm = Thm.combination thm (Thm.reflexive free)
-      |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
-      |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
-  in
-    ct
-    |> fold_rev Thm.cabs frees
-    |> conv
-    |> fold apply_beta frees
-  end;
-
-
 (* dedicated simpset *)
 
 structure Simpset = Theory_Data
@@ -68,8 +51,8 @@
 
 (* evaluation with dynamic code context *)
 
-val dynamic_eval_conv = Conv.tap_thy (fn thy => no_frees_conv (Code_Thingol.dynamic_eval_conv thy
-  (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program)));
+val dynamic_eval_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy
+  (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
 
 fun dynamic_eval_tac thy = CONVERSION dynamic_eval_conv THEN' conclude_tac thy NONE;
 
@@ -83,9 +66,9 @@
 
 (* evaluation with static code context *)
 
-fun static_eval_conv thy some_ss consts = no_frees_conv
-  (Code_Thingol.static_eval_conv_simple thy consts
-    (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program));
+fun static_eval_conv thy some_ss consts =
+  Code_Thingol.static_eval_conv_simple thy consts
+    (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program);
 
 fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
   THEN' conclude_tac thy some_ss;
diff -r ae2c3059f8cc -r e5448cf9a048 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Wed Sep 22 10:02:39 2010 +0200
+++ b/src/Tools/nbe.ML	Wed Sep 22 11:46:28 2010 +0200
@@ -589,28 +589,18 @@
 fun oracle thy program nbe_program_idx_tab vsp_ty_t deps ct =
   raw_oracle (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct);
 
-fun no_frees_rew rew t =
-  let
-    val frees = map Free (Term.add_frees t []);
-  in
-    t
-    |> fold_rev lambda frees
-    |> rew
-    |> curry (Term.betapplys o swap) frees
-  end;
-
-val dynamic_eval_conv = Conv.tap_thy (fn thy => Code_Simp.no_frees_conv
-  (lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy
-    (K (fn program => oracle thy program (compile false thy program))))));
+val dynamic_eval_conv = Conv.tap_thy (fn thy =>
+  lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy
+    (K (fn program => oracle thy program (compile false thy program)))));
 
 fun dynamic_eval_value thy = lift_triv_classes_rew thy
-  (no_frees_rew (Code_Thingol.dynamic_eval_value thy I
-    (K (fn program => eval_term thy program (compile false thy program)))));
+  (Code_Thingol.dynamic_eval_value thy I
+    (K (fn program => eval_term thy program (compile false thy program))));
 
-fun static_eval_conv thy consts = Code_Simp.no_frees_conv
-  (lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
+fun static_eval_conv thy consts =
+  lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
     (K (fn program => let val nbe_program = compile true thy program
-      in fn thy => oracle thy program nbe_program end))));
+      in fn thy => oracle thy program nbe_program end)));
 
 
 (** setup **)