
diff -r a2dde53b15ef -r 56fad09655a5 doc-src/IsarImplementation/Thy/Prelim.thy
--- 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}
 *}
 




