diff -r 465851ba524e -r a1827b8b45ae doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat Feb 04 18:33:04 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sun Feb 05 18:11:19 2012 +0100
@@ -974,6 +974,45 @@
 *}
 
 
+subsection {* Ambiguity of parsed expressions *}
+
+text {*
+  \begin{tabular}{rcll}
+    @{attribute_def syntax_ambiguity_level} & : & @{text attribute} & default @{text 1} \\
+  \end{tabular}
+
+  \begin{mldecls}
+    @{index_ML Syntax.ambiguity_limit: "int Config.T"} \\  %FIXME attribute
+  \end{mldecls}
+
+  Depending on the grammar and the given input, parsing may be
+  ambiguous.  Isabelle lets the Earley parser enumerate all possible
+  parse trees, and then tries to make the best out of the situation.
+  Terms that cannot be type-checked are filtered out, which often
+  leads to a unique result in the end.  Unlike regular type
+  reconstruction, which is applied to the whole collection of input
+  terms simultaneously, the filtering stage only treats each given
+  term in isolation.  Filtering is also not attempted for individual
+  types or raw ASTs (as required for @{command translations}).
+
+  Certain warning or error messages are printed, depending on the
+  situation and the given configuration options.  Parsing ultimately
+  fails, if multiple results remain after the filtering phase.
+
+  \begin{description}
+
+  \item @{attribute syntax_ambiguity_level} determines the number of
+  parser results that are tolerated without printing a detailed
+  message.
+
+  \item @{ML Syntax.ambiguity_limit} determines the number of
+  resulting parse trees that are shown as part of the printed message
+  in case of an ambiguity.
+
+  \end{description}
+*}
+
+
 section {* Raw syntax and translations \label{sec:syn-trans} *}
 
 text {*