salvaged some ML functors from decay, which is the natural consequence of lack of formal checking;
--- a/doc-src/IsarImplementation/Thy/ML.thy Fri Apr 16 11:39:08 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Fri Apr 16 11:40:01 2010 +0200
@@ -209,7 +209,7 @@
options} for type @{ML_type "bool"}/@{ML_type "int"}/@{ML_type
"string"} (see structure @{ML_struct Config} and @{ML
Attrib.config_bool} etc.), and lists of theorems (see functor
- @{ML_functor NamedThmsFun}).
+ @{ML_functor Named_Thms}).
\item Keep components with local state information
\emph{re-entrant}. Instead of poking initial values into (private)
@@ -623,7 +623,7 @@
whenever such pure finite mappings are neccessary.
The key type of tables must be given explicitly by instantiating
- the @{ML_functor TableFun} functor which takes the key type
+ the @{ML_functor Table} functor which takes the key type
together with its @{ML_type order}; for convience, we restrict
here to the @{ML_struct Symtab} instance with @{ML_type string}
as key type.
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Fri Apr 16 11:39:08 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Fri Apr 16 11:40:01 2010 +0200
@@ -222,7 +222,7 @@
\secref{sec:context-data}) there are drop-in replacements that
emulate primitive references for common cases of \emph{configuration
options} for type \verb|bool|/\verb|int|/\verb|string| (see structure \verb|Config| and \verb|Attrib.config_bool| etc.), and lists of theorems (see functor
- \verb|NamedThmsFun|).
+ \verb|Named_Thms|).
\item Keep components with local state information
\emph{re-entrant}. Instead of poking initial values into (private)
@@ -763,7 +763,7 @@
whenever such pure finite mappings are neccessary.
The key type of tables must be given explicitly by instantiating
- the \verb|TableFun| functor which takes the key type
+ the \verb|Table| functor which takes the key type
together with its \verb|order|; for convience, we restrict
here to the \verb|Symtab| instance with \verb|string|
as key type.