--- a/doc-src/IsarImplementation/Thy/Prelim.thy Thu Oct 28 22:59:33 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Thu Oct 28 23:19:52 2010 +0200
@@ -226,11 +226,10 @@
text %mlantiq {*
\begin{matharray}{rcl}
@{ML_antiquotation_def "theory"} & : & @{text ML_antiquotation} \\
- @{ML_antiquotation_def "theory_ref"} & : & @{text ML_antiquotation} \\
\end{matharray}
\begin{rail}
- ('theory' | 'theory\_ref') nameref?
+ 'theory' nameref?
;
\end{rail}
@@ -243,10 +242,6 @@
theory @{text "A"} of the background theory of the current context
--- as abstract value.
- \item @{text "@{theory_ref}"} is similar to @{text "@{theory}"}, but
- produces a @{ML_type theory_ref} via @{ML "Theory.check_thy"} as
- explained above.
-
\end{description}
*}