# HG changeset patch
# User wenzelm
# Date 1271410801 -7200
# Node ID 532f4d1cb0fca1c48cb20c5626a2e0f147276b20
# Parent  823c9400eb62c6d4bc6b5c5d28e096704fe9e461
salvaged some ML functors from decay, which is the natural consequence of lack of formal checking;

diff -r 823c9400eb62 -r 532f4d1cb0fc doc-src/IsarImplementation/Thy/ML.thy
--- 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.
diff -r 823c9400eb62 -r 532f4d1cb0fc doc-src/IsarImplementation/Thy/document/ML.tex
--- 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.