'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';

--- a/NEWS	Wed Aug 22 21:43:17 2012 +0200
+++ b/NEWS	Wed Aug 22 22:47:16 2012 +0200
@@ -6,6 +6,9 @@
 
 *** General ***
 
+* Command 'ML_file' evaluates ML text from a file directly within the
+theory, without any predeclaration via 'uses' in the theory header.
+
 * Discontinued obsolete method fastsimp / tactic fast_simp_tac, which
 is called fastforce / fast_force_tac already since Isabelle2011-1.
 

--- a/doc-src/IsarRef/Thy/Spec.thy	Wed Aug 22 21:43:17 2012 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Aug 22 22:47:16 2012 +0200
@@ -960,7 +960,7 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def "use"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+    @{command_def "ML_file"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\
     @{command_def "ML_val"} & : & @{text "any \<rightarrow>"} \\
@@ -971,7 +971,7 @@
   \end{matharray}
 
   @{rail "
-    @@{command use} @{syntax name}
+    @@{command ML_file} @{syntax name}
     ;
     (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
       @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
@@ -981,28 +981,22 @@
 
   \begin{description}
 
-  \item @{command "use"}~@{text "file"} reads and executes ML
-  commands from @{text "file"}.  The current theory context is passed
-  down to the ML toplevel and may be modified, using @{ML
-  "Context.>>"} or derived ML commands.  The file name is checked with
-  the @{keyword_ref "uses"} dependency declaration given in the theory
-  header (see also \secref{sec:begin-thy}).
-
-  Top-level ML bindings are stored within the (global or local) theory
-  context.
+  \item @{command "ML_file"}~@{text "name"} reads and evaluates the
+  given ML file.  The current theory context is passed down to the ML
+  toplevel and may be modified, using @{ML "Context.>>"} or derived ML
+  commands.  Top-level ML bindings are stored within the (global or
+  local) theory context.
   
-  \item @{command "ML"}~@{text "text"} is similar to @{command "use"},
-  but executes ML commands directly from the given @{text "text"}.
+  \item @{command "ML"}~@{text "text"} is similar to @{command
+  "ML_file"}, but evaluates directly the given @{text "text"}.
   Top-level ML bindings are stored within the (global or local) theory
   context.
 
   \item @{command "ML_prf"} is analogous to @{command "ML"} but works
-  within a proof context.
-
-  Top-level ML bindings are stored within the proof context in a
-  purely sequential fashion, disregarding the nested proof structure.
-  ML bindings introduced by @{command "ML_prf"} are discarded at the
-  end of the proof.
+  within a proof context.  Top-level ML bindings are stored within the
+  proof context in a purely sequential fashion, disregarding the
+  nested proof structure.  ML bindings introduced by @{command
+  "ML_prf"} are discarded at the end of the proof.
 
   \item @{command "ML_val"} and @{command "ML_command"} are diagnostic
   versions of @{command "ML"}, which means that the context may not be

--- a/doc-src/IsarRef/Thy/document/Spec.tex	Wed Aug 22 21:43:17 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Wed Aug 22 22:47:16 2012 +0200
@@ -1444,7 +1444,7 @@
 %
 \begin{isamarkuptext}%
 \begin{matharray}{rcl}
-    \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{}{command}{ML\_file}\hypertarget{command.ML-file}{\hyperlink{command.ML-file}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}file}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{}{command}{ML\_prf}\hypertarget{command.ML-prf}{\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
@@ -1456,7 +1456,7 @@
 
   \begin{railoutput}
 \rail@begin{1}{}
-\rail@term{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}}[]
+\rail@term{\hyperlink{command.ML-file}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}file}}}}}[]
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
 \rail@end
 \rail@begin{6}{}
@@ -1490,27 +1490,20 @@
 
   \begin{description}
 
-  \item \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}file{\isaliteral{22}{\isachardoublequote}}} reads and executes ML
-  commands from \isa{{\isaliteral{22}{\isachardoublequote}}file{\isaliteral{22}{\isachardoublequote}}}.  The current theory context is passed
-  down to the ML toplevel and may be modified, using \verb|Context.>>| or derived ML commands.  The file name is checked with
-  the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}} dependency declaration given in the theory
-  header (see also \secref{sec:begin-thy}).
-
-  Top-level ML bindings are stored within the (global or local) theory
-  context.
+  \item \hyperlink{command.ML-file}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}file}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{22}{\isachardoublequote}}} reads and evaluates the
+  given ML file.  The current theory context is passed down to the ML
+  toplevel and may be modified, using \verb|Context.>>| or derived ML
+  commands.  Top-level ML bindings are stored within the (global or
+  local) theory context.
   
-  \item \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}},
-  but executes ML commands directly from the given \isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}}.
+  \item \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} is similar to \hyperlink{command.ML-file}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}file}}}}, but evaluates directly the given \isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}}.
   Top-level ML bindings are stored within the (global or local) theory
   context.
 
   \item \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}} is analogous to \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} but works
-  within a proof context.
-
-  Top-level ML bindings are stored within the proof context in a
-  purely sequential fashion, disregarding the nested proof structure.
-  ML bindings introduced by \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}} are discarded at the
-  end of the proof.
+  within a proof context.  Top-level ML bindings are stored within the
+  proof context in a purely sequential fashion, disregarding the
+  nested proof structure.  ML bindings introduced by \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}} are discarded at the end of the proof.
 
   \item \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}} are diagnostic
   versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context may not be