diff -r a2dde53b15ef -r 56fad09655a5 doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Thu Oct 28 22:59:33 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Thu Oct 28 23:19:52 2010 +0200
@@ -262,11 +262,10 @@
 \begin{isamarkuptext}%
 \begin{matharray}{rcl}
   \indexdef{}{ML antiquotation}{theory}\hypertarget{ML antiquotation.theory}{\hyperlink{ML antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
-  \indexdef{}{ML antiquotation}{theory\_ref}\hypertarget{ML antiquotation.theory-ref}{\hyperlink{ML antiquotation.theory-ref}{\mbox{\isa{theory{\isacharunderscore}ref}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
   \end{matharray}
 
   \begin{rail}
-  ('theory' | 'theory\_ref') nameref?
+  'theory' nameref?
   ;
   \end{rail}
 
@@ -279,10 +278,6 @@
   theory \isa{A} of the background theory of the current context
   --- as abstract value.
 
-  \item \isa{{\isacharat}{\isacharbraceleft}theory{\isacharunderscore}ref{\isacharbraceright}} is similar to \isa{{\isacharat}{\isacharbraceleft}theory{\isacharbraceright}}, but
-  produces a \verb|theory_ref| via \verb|Theory.check_thy| as
-  explained above.
-
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%