# HG changeset patch
# User wenzelm
# Date 1206478039 -3600
# Node ID c08a5ab37fcd3cd29539e8939b1f6adedb06eaba
# Parent  fccb74555d9e956521f0b9a6a47933e8bcde6613
added command 'ML_val' (presently just a clone of 'ML');

diff -r fccb74555d9e -r c08a5ab37fcd doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Tue Mar 25 21:28:39 2008 +0100
+++ b/doc-src/IsarRef/pure.tex	Tue Mar 25 21:47:19 2008 +0100
@@ -466,35 +466,28 @@
 
 \subsection{Incorporating ML code}\label{sec:ML}
 
-\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{ML-command}
+\indexisarcmd{use}\indexisarcmd{ML}
+\indexisarcmd{ML-val}\indexisarcmd{ML-command}
 \indexisarcmd{ML-setup}\indexisarcmd{setup}
 \indexisarcmd{method-setup}
 \begin{matharray}{rcl}
   \isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
   \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
+  \isarcmd{ML_val} & : & \isartrans{\cdot}{\cdot} \\
   \isarcmd{ML_command} & : & \isartrans{\cdot}{\cdot} \\
   \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
   \isarcmd{setup} & : & \isartrans{theory}{theory} \\
   \isarcmd{method_setup} & : & \isartrans{theory}{theory} \\
 \end{matharray}
 
-\railalias{MLsetup}{ML\_setup}
-\railterm{MLsetup}
-
-\railalias{methodsetup}{method\_setup}
-\railterm{methodsetup}
-
-\railalias{MLcommand}{ML\_command}
-\railterm{MLcommand}
-
 \begin{rail}
   'use' name
   ;
-  ('ML' | MLcommand | MLsetup) text
+  ('ML' | 'ML\_val' | 'ML\_command' | 'ML\_setup') text
   ;
   'setup' text?
   ;
-  methodsetup name '=' text text
+  'method\_setup' name '=' text text
   ;
 \end{rail}
 
@@ -505,10 +498,12 @@
   $\isarkeyword{files}$ dependency declaration given in the theory header (see
   also \S\ref{sec:begin-thy}).
   
-\item [$\isarkeyword{ML}~text$ and $\isarkeyword{ML_command}~text$] execute ML
-  commands from $text$.  The theory context is passed in the same way as for
-  $\isarkeyword{use}$, but may not be changed.  Note that the output of
-  $\isarkeyword{ML_command}$ is less verbose than plain $\isarkeyword{ML}$.
+\item [$\isarkeyword{ML}~text$ and $\isarkeyword{ML_val}~text$ and
+  $\isarkeyword{ML_command}~text$] execute ML commands from $text$.
+  The theory context is passed in the same way as for
+  $\isarkeyword{use}$, but may not be changed.  Note that the output
+  of $\isarkeyword{ML_command}$ is less verbose than plain
+  $\isarkeyword{ML}$.
   
 \item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$.  The
   theory context is passed down to the ML session, and fetched back