diff -r fbb3c68a8d3c -r 4f9f61f9b535 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Feb 17 11:24:39 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Fri Feb 17 15:42:26 2012 +0100
@@ -980,7 +980,7 @@
 
 text {*
   \begin{tabular}{rcll}
-    @{attribute_def syntax_ambiguity} & : & @{text attribute} & default @{text warning} \\
+    @{attribute_def syntax_ambiguity_warning} & : & @{text attribute} & default @{text true} \\
     @{attribute_def syntax_ambiguity_limit} & : & @{text attribute} & default @{text 10} \\
   \end{tabular}
 
@@ -1000,9 +1000,8 @@
 
   \begin{description}
 
-  \item @{attribute syntax_ambiguity} determines reaction on multiple
-  results of parsing; this string option can be set to @{text
-  "ignore"}, @{text "warning"}, or @{text "error"}.
+  \item @{attribute syntax_ambiguity_warning} controls output of
+  explicit warning messages about syntax ambiguity.
 
   \item @{attribute syntax_ambiguity_limit} determines the number of
   resulting parse trees that are shown as part of the printed message