src/Pure/Syntax/syntax.ML

 signature SYNTAX =
 sig
   type operations
   val install_operations: operations -> theory -> theory
   val root: string Config.T
-  val ambiguity_warning_raw: Config.raw
   val ambiguity_warning: bool Config.T
-  val ambiguity_limit_raw: Config.raw
   val ambiguity_limit: int Config.T
   val encode_input: Input.source -> XML.tree
   val implode_input: Input.source -> string
   val read_input_pos: string -> Position.T
   val read_input: string -> Input.source

   | SOME ops => which ops ctxt x);
 
 
 (* configuration options *)
 
-val root = Config.string (Config.declare ("syntax_root", \<^here>) (K (Config.String "any")));
-
-val ambiguity_warning_raw =
-  Config.declare ("syntax_ambiguity_warning", \<^here>) (fn _ => Config.Bool true);
-val ambiguity_warning = Config.bool ambiguity_warning_raw;
-
-val ambiguity_limit_raw =
-  Config.declare ("syntax_ambiguity_limit", \<^here>) (fn _ => Config.Int 10);
-val ambiguity_limit = Config.int ambiguity_limit_raw;
+val root = Config.declare_string ("syntax_root", \<^here>) (K "any");
+val ambiguity_warning = Config.declare_bool ("syntax_ambiguity_warning", \<^here>) (K true);
+val ambiguity_limit = Config.declare_int ("syntax_ambiguity_limit", \<^here>) (K 10);
 
 
 (* formal input *)
 
 fun encode_input source =

 val string_of_arity = Pretty.string_of oo pretty_arity;
 
 
 (* global pretty printing *)
 
-val pretty_global =
-  Config.bool (Config.declare ("Syntax.pretty_global", \<^here>) (K (Config.Bool false)));
+val pretty_global = Config.declare_bool ("Syntax.pretty_global", \<^here>) (K false);
 fun is_pretty_global ctxt = Config.get ctxt pretty_global;
 val set_pretty_global = Config.put pretty_global;
 val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
 val init_pretty = Context.cases init_pretty_global I;