configuration options Syntax.ambiguity_enabled (inverse of former Syntax.ambiguity_is_error), Syntax.ambiguity_level (with Isar attribute "syntax_ambiguity_level"), Syntax.ambiguity_limit;

--- a/NEWS	Fri Sep 03 21:13:53 2010 +0200
+++ b/NEWS	Fri Sep 03 22:36:16 2010 +0200
@@ -30,18 +30,20 @@
 
   ML (Config.T)                 Isar (attribute)
 
+  show_question_marks           show_question_marks
+  show_consts                   show_consts
+
+  Syntax.ambiguity_level        syntax_ambiguity_level
+
+  Goal_Display.goals_limit      goals_limit
+  Goal_Display.show_main_goal   show_main_goal
+
   Thy_Output.display            thy_output_display
   Thy_Output.quotes             thy_output_quotes
   Thy_Output.indent             thy_output_indent
   Thy_Output.source             thy_output_source
   Thy_Output.break              thy_output_break
 
-  show_question_marks           show_question_marks
-  show_consts                   show_consts
-
-  Goal_Display.goals_limit      goals_limit
-  Goal_Display.show_main_goal   show_main_goal
-
 Note that corresponding "..._default" references in ML may be only
 changed globally at the ROOT session setup, but *not* within a theory.
 

--- a/src/HOL/Import/proof_kernel.ML	Fri Sep 03 21:13:53 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Fri Sep 03 22:36:16 2010 +0200
@@ -189,7 +189,9 @@
 
 fun simple_smart_string_of_cterm ctxt0 ct =
     let
-        val ctxt = Config.put show_all_types true ctxt0;
+        val ctxt = ctxt0
+          |> Config.put show_all_types true
+          |> Config.put Syntax.ambiguity_enabled true;
         val {t,T,...} = rep_cterm ct
         (* Hack to avoid parse errors with Trueprop *)
         val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
@@ -198,15 +200,15 @@
         quote (
         Print_Mode.setmp [] (
         setmp_CRITICAL show_brackets false (
-        setmp_CRITICAL Syntax.ambiguity_is_error false (
-        setmp_CRITICAL show_sorts true (Syntax.string_of_term ctxt o Thm.term_of))))
+        setmp_CRITICAL show_sorts true (Syntax.string_of_term ctxt o Thm.term_of)))
         ct)
     end
 
 exception SMART_STRING
 
-fun smart_string_of_cterm ctxt ct =
+fun smart_string_of_cterm ctxt0 ct =
     let
+        val ctxt = ctxt0 |> Config.put Syntax.ambiguity_enabled false;
         val {t,T,...} = rep_cterm ct
         (* Hack to avoid parse errors with Trueprop *)
         val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
@@ -232,9 +234,9 @@
               | SMART_STRING =>
                   error ("smart_string failed for: "^ G 0 Syntax.string_of_term ctxt (term_of ct))
     in
-      Print_Mode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
+      Print_Mode.setmp [] F 0
     end
-    handle ERROR mesg => simple_smart_string_of_cterm ctxt ct
+    handle ERROR mesg => simple_smart_string_of_cterm ctxt0 ct
 
 fun smart_string_of_thm ctxt = smart_string_of_cterm ctxt o cprop_of
 

--- a/src/HOL/Lambda/Commutation.thy	Fri Sep 03 21:13:53 2010 +0200
+++ b/src/HOL/Lambda/Commutation.thy	Fri Sep 03 22:36:16 2010 +0200
@@ -7,6 +7,9 @@
 
 theory Commutation imports Main begin
 
+declare [[syntax_ambiguity_level = 100]]
+
+
 subsection {* Basic definitions *}
 
 definition

--- a/src/HOL/Lambda/Lambda.thy	Fri Sep 03 21:13:53 2010 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Fri Sep 03 22:36:16 2010 +0200
@@ -7,6 +7,8 @@
 
 theory Lambda imports Main begin
 
+declare [[syntax_ambiguity_level = 100]]
+
 
 subsection {* Lambda-terms in de Bruijn notation and substitution *}
 

--- a/src/HOL/Lambda/ListOrder.thy	Fri Sep 03 21:13:53 2010 +0200
+++ b/src/HOL/Lambda/ListOrder.thy	Fri Sep 03 22:36:16 2010 +0200
@@ -7,6 +7,9 @@
 
 theory ListOrder imports Main begin
 
+declare [[syntax_ambiguity_level = 100]]
+
+
 text {*
   Lifting an order to lists of elements, relating exactly one
   element.

--- a/src/HOL/Lambda/ROOT.ML	Fri Sep 03 21:13:53 2010 +0200
+++ b/src/HOL/Lambda/ROOT.ML	Fri Sep 03 22:36:16 2010 +0200
@@ -1,4 +1,2 @@
-Syntax.ambiguity_level := 100;
-
 no_document use_thys ["Code_Integer"];
 use_thys ["Eta", "StrongNorm", "Standardization", "WeakNorm"];

--- a/src/HOL/MicroJava/J/JListExample.thy	Fri Sep 03 21:13:53 2010 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Fri Sep 03 22:36:16 2010 +0200
@@ -8,7 +8,7 @@
 imports Eval
 begin
 
-ML {* Syntax.ambiguity_level := 100000 *}
+declare [[syntax_ambiguity_level = 100000]]
 
 consts
   list_name :: cname

--- a/src/Pure/Isar/attrib.ML	Fri Sep 03 21:13:53 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Sep 03 22:36:16 2010 +0200
@@ -393,6 +393,7 @@
 
 val _ = Context.>> (Context.map_theory
  (register_config Syntax.show_question_marks_value #>
+  register_config Syntax.ambiguity_level_value #>
   register_config Goal_Display.goals_limit_value #>
   register_config Goal_Display.show_main_goal_value #>
   register_config Goal_Display.show_consts_value #>

--- a/src/Pure/Syntax/syntax.ML	Fri Sep 03 21:13:53 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Sep 03 22:36:16 2010 +0200
@@ -36,9 +36,10 @@
   val print_syntax: syntax -> unit
   val guess_infix: syntax -> string -> mixfix option
   val read_token: string -> Symbol_Pos.T list * Position.T
-  val ambiguity_is_error: bool Unsynchronized.ref
-  val ambiguity_level: int Unsynchronized.ref
-  val ambiguity_limit: int Unsynchronized.ref
+  val ambiguity_enabled: bool Config.T
+  val ambiguity_level_value: Config.value Config.T
+  val ambiguity_level: int Config.T
+  val ambiguity_limit: int Config.T
   val standard_parse_term: Pretty.pp -> (term -> string option) ->
     (((string * int) * sort) list -> string * int -> Term.sort) ->
     (string -> bool * string) -> (string -> string option) -> Proof.context ->
@@ -472,9 +473,14 @@
 
 (* read_ast *)
 
-val ambiguity_is_error = Unsynchronized.ref false;
-val ambiguity_level = Unsynchronized.ref 1;
-val ambiguity_limit = Unsynchronized.ref 10;
+val ambiguity_enabled =
+  Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true));
+
+val ambiguity_level_value = Config.declare "syntax_ambiguity_level" (fn _ => Config.Int 1);
+val ambiguity_level = Config.int ambiguity_level_value;
+
+val ambiguity_limit =
+  Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
 
 fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
 
@@ -488,12 +494,12 @@
     val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks);
     val len = length pts;
 
-    val limit = ! ambiguity_limit;
+    val limit = Config.get ctxt ambiguity_limit;
     fun show_pt pt =
       Pretty.string_of (Ast.pretty_ast (hd (Syn_Trans.pts_to_asts ctxt (K NONE) [pt])));
   in
-    if len <= ! ambiguity_level then ()
-    else if ! ambiguity_is_error then error (ambiguity_msg pos)
+    if len <= Config.get ctxt ambiguity_level then ()
+    else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
     else
       (Context_Position.if_visible ctxt warning (cat_lines
         (("Ambiguous input" ^ Position.str_of pos ^
@@ -522,14 +528,14 @@
 fun disambig _ _ _ [t] = t
   | disambig ctxt pp check ts =
       let
-        val level = ! ambiguity_level;
-        val limit = ! ambiguity_limit;
+        val level = Config.get ctxt ambiguity_level;
+        val limit = Config.get ctxt ambiguity_limit;
 
         val ambiguity = length ts;
         fun ambig_msg () =
           if ambiguity > 1 andalso ambiguity <= level then
             "Got more than one parse tree.\n\
-            \Retry with smaller Syntax.ambiguity_level for more information."
+            \Retry with smaller syntax_ambiguity_level for more information."
           else "";
 
         val errs = Par_List.map check ts;