src/Pure/Syntax/syntax.ML

--- a/src/Pure/Syntax/syntax.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Syntax/syntax.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -10,9 +10,7 @@
   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
@@ -161,15 +159,9 @@
 
 (* 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 *)
@@ -330,8 +322,7 @@
 
 (* 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;