diff -r 350857040d09 -r 1080dee73a53 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Oct 09 19:49:19 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Oct 09 21:04:03 2010 +0100
@@ -211,6 +211,33 @@
   \end{description}
 *}
 
+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?
+  ;
+  \end{rail}
+
+  \begin{description}
+
+  \item @{text "@{theory}"} refers to the background theory of the
+  current context --- as abstract value.
+
+  \item @{text "@{theory A}"} refers to an explicitly named ancestor
+  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}
+*}
+
 
 subsection {* Proof context \label{sec:context-proof} *}
 
@@ -270,6 +297,23 @@
   \end{description}
 *}
 
+text %mlantiq {*
+  \begin{matharray}{rcl}
+  @{ML_antiquotation_def "context"} & : & @{text ML_antiquotation} \\
+  \end{matharray}
+
+  \begin{description}
+
+  \item @{text "@{context}"} refers to \emph{the} context at
+  compile-time --- as abstract value.  Independently of (local) theory
+  or proof mode, this always produces a meaningful result.
+
+  This is probably the most common antiquotation in interactive
+  experimentation with ML inside Isar.
+
+  \end{description}
+*}
+
 
 subsection {* Generic contexts \label{sec:generic-context} *}
 
@@ -916,7 +960,9 @@
   \item @{ML Binding.empty} is the empty binding.
 
   \item @{ML Binding.name}~@{text "name"} produces a binding with base
-  name @{text "name"}.
+  name @{text "name"}.  Note that this lacks proper source position
+  information; see also the ML antiquotation @{ML_antiquotation
+  binding}.
 
   \item @{ML Binding.qualify}~@{text "mandatory name binding"}
   prefixes qualifier @{text "name"} to @{text "binding"}.  The @{text
@@ -990,4 +1036,24 @@
   \end{description}
 *}
 
+text %mlantiq {*
+  \begin{matharray}{rcl}
+  @{ML_antiquotation_def "binding"} & : & @{text ML_antiquotation} \\
+  \end{matharray}
+
+  \begin{rail}
+  'binding' name
+  ;
+  \end{rail}
+
+  \begin{description}
+
+  \item @{text "@{binding name}"} produces a binding with base name
+  @{text "name"} and the source position taken from the concrete
+  syntax of this antiquotation.  In many situations this is more
+  appropriate than the more basic @{ML Binding.name} function.
+
+  \end{description}
+*}
+
 end