diff -r dc0a73004c94 -r d7c7ec248ef0 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Aug 08 11:47:41 2011 -0700
+++ b/src/Pure/Syntax/syntax.ML	Sat Aug 06 15:48:08 2011 +0200
@@ -16,6 +16,8 @@
   val ambiguity_level_raw: Config.raw
   val ambiguity_level: int Config.T
   val ambiguity_limit: int Config.T
+  val ambiguity_warnings_raw: Config.raw
+  val ambiguity_warnings: bool Config.T
   val read_token: string -> Symbol_Pos.T list * Position.T
   val parse_token: Proof.context -> (XML.tree list -> 'a) ->
     Markup.T -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
@@ -193,6 +195,11 @@
 val ambiguity_limit =
   Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
 
+val ambiguity_warnings_raw = 
+  Config.declare "syntax_ambiguity_warnings" (fn _ => Config.Bool true);
+val ambiguity_warnings =
+  Config.bool ambiguity_warnings_raw;
+
 
 (* outer syntax token -- with optional YXML content *)