diff -r e28b5d8f5613 -r ded41f584938 src/Doc/IsarRef/Spec.thy
--- a/src/Doc/IsarRef/Spec.thy	Mon Sep 10 12:00:28 2012 +0200
+++ b/src/Doc/IsarRef/Spec.thy	Mon Sep 10 12:13:39 2012 +0200
@@ -51,13 +51,11 @@
   admissible.
 
   @{rail "
-    @@{command theory} @{syntax name} imports \\ keywords? uses? @'begin'
+    @@{command theory} @{syntax name} imports keywords? \\ @'begin'
     ;
     imports: @'imports' (@{syntax name} +)
     ;
     keywords: @'keywords' ((@{syntax string} +) ('::' @{syntax name} @{syntax tags})? + @'and')
-    ;
-    uses: @'uses' ((@{syntax name} | @{syntax parname}) +)
   "}
 
   \begin{description}
@@ -84,14 +82,6 @@
   with and without proof, respectively.  Additional @{syntax tags}
   provide defaults for document preparation (\secref{sec:tags}).
   
-  The optional @{keyword_def "uses"} specification declares additional
-  dependencies on external files (notably ML sources).  Files will be
-  loaded immediately (as ML), unless the name is parenthesized.  The
-  latter case records a dependency that needs to be resolved later in
-  the text, usually via explicit @{command_ref "use"} for ML files;
-  other file formats require specific load commands defined by the
-  corresponding tools or packages.
-  
   \item @{command (global) "end"} concludes the current theory
   definition.  Note that some other commands, e.g.\ local theory
   targets @{command locale} or @{command class} may involve a