# HG changeset patch
# User wenzelm
# Date 1546521164 -3600
# Node ID f77cc54f6d47b577e05e0915e7358e3fdfe49bf2
# Parent  b4ea943ce0b7f63e43d914e783bac46455bf74b1
clarified signature: more types;

diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/General/name_space.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -19,11 +19,8 @@
   val entry_ord: T -> string * string -> order
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
-  val names_long_raw: Config.raw
   val names_long: bool Config.T
-  val names_short_raw: Config.raw
   val names_short: bool Config.T
-  val names_unique_raw: Config.raw
   val names_unique: bool Config.T
   val extern: Proof.context -> T -> string -> xstring
   val extern_ord: Proof.context -> T -> string * string -> order
@@ -215,14 +212,9 @@
 
 (* extern *)
 
-val names_long_raw = Config.declare_option ("names_long", \<^here>);
-val names_long = Config.bool names_long_raw;
-
-val names_short_raw = Config.declare_option ("names_short", \<^here>);
-val names_short = Config.bool names_short_raw;
-
-val names_unique_raw = Config.declare_option ("names_unique", \<^here>);
-val names_unique = Config.bool names_unique_raw;
+val names_long = Config.declare_option_bool ("names_long", \<^here>);
+val names_short = Config.declare_option_bool ("names_short", \<^here>);
+val names_unique = Config.declare_option_bool ("names_unique", \<^here>);
 
 fun extern ctxt space name =
   let
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Isar/attrib.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -380,7 +380,7 @@
 
 structure Configs = Theory_Data
 (
-  type T = Config.raw Symtab.table;
+  type T = Config.value Config.T Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
   fun merge data = Symtab.merge (K true) data;
@@ -438,6 +438,11 @@
 fun register_config config =
   register (Binding.make (Config.name_of config, Config.pos_of config)) config;
 
+val register_config_bool = register_config o Config.bool_value;
+val register_config_int = register_config o Config.int_value;
+val register_config_real = register_config o Config.real_value;
+val register_config_string = register_config o Config.string_value;
+
 val config_bool = declare Config.Bool Config.bool;
 val config_int = declare Config.Int Config.int;
 val config_real = declare Config.Real Config.real;
@@ -572,45 +577,45 @@
     (Scan.succeed (Thm.rule_attribute [] (Local_Defs.abs_def_rule o Context.proof_of)))
     "abstract over free variables of definitional theorem" #>
 
-  register_config Goal.quick_and_dirty_raw #>
-  register_config Ast.trace_raw #>
-  register_config Ast.stats_raw #>
-  register_config Printer.show_brackets_raw #>
-  register_config Printer.show_sorts_raw #>
-  register_config Printer.show_types_raw #>
-  register_config Printer.show_markup_raw #>
-  register_config Printer.show_structs_raw #>
-  register_config Printer.show_question_marks_raw #>
-  register_config Syntax.ambiguity_warning_raw #>
-  register_config Syntax.ambiguity_limit_raw #>
-  register_config Syntax_Trans.eta_contract_raw #>
-  register_config Name_Space.names_long_raw #>
-  register_config Name_Space.names_short_raw #>
-  register_config Name_Space.names_unique_raw #>
-  register_config ML_Print_Depth.print_depth_raw #>
-  register_config ML_Env.ML_environment_raw #>
-  register_config ML_Env.ML_read_global_raw #>
-  register_config ML_Env.ML_write_global_raw #>
-  register_config ML_Options.source_trace_raw #>
-  register_config ML_Options.exception_trace_raw #>
-  register_config ML_Options.exception_debugger_raw #>
-  register_config ML_Options.debugger_raw #>
-  register_config Proof_Context.show_abbrevs_raw #>
-  register_config Goal_Display.goals_limit_raw #>
-  register_config Goal_Display.show_main_goal_raw #>
-  register_config Thm.show_consts_raw #>
-  register_config Thm.show_hyps_raw #>
-  register_config Thm.show_tags_raw #>
-  register_config Pattern.unify_trace_failure_raw #>
-  register_config Unify.trace_bound_raw #>
-  register_config Unify.search_bound_raw #>
-  register_config Unify.trace_simp_raw #>
-  register_config Unify.trace_types_raw #>
-  register_config Raw_Simplifier.simp_depth_limit_raw #>
-  register_config Raw_Simplifier.simp_trace_depth_limit_raw #>
-  register_config Raw_Simplifier.simp_debug_raw #>
-  register_config Raw_Simplifier.simp_trace_raw #>
-  register_config Local_Defs.unfold_abs_def_raw);
+  register_config_bool Goal.quick_and_dirty #>
+  register_config_bool Ast.trace #>
+  register_config_bool Ast.stats #>
+  register_config_bool Printer.show_brackets #>
+  register_config_bool Printer.show_sorts #>
+  register_config_bool Printer.show_types #>
+  register_config_bool Printer.show_markup #>
+  register_config_bool Printer.show_structs #>
+  register_config_bool Printer.show_question_marks #>
+  register_config_bool Syntax.ambiguity_warning #>
+  register_config_int Syntax.ambiguity_limit #>
+  register_config_bool Syntax_Trans.eta_contract #>
+  register_config_bool Name_Space.names_long #>
+  register_config_bool Name_Space.names_short #>
+  register_config_bool Name_Space.names_unique #>
+  register_config_int ML_Print_Depth.print_depth #>
+  register_config_string ML_Env.ML_environment #>
+  register_config_bool ML_Env.ML_read_global #>
+  register_config_bool ML_Env.ML_write_global #>
+  register_config_bool ML_Options.source_trace #>
+  register_config_bool ML_Options.exception_trace #>
+  register_config_bool ML_Options.exception_debugger #>
+  register_config_bool ML_Options.debugger #>
+  register_config_bool Proof_Context.show_abbrevs #>
+  register_config_int Goal_Display.goals_limit #>
+  register_config_bool Goal_Display.show_main_goal #>
+  register_config_bool Thm.show_consts #>
+  register_config_bool Thm.show_hyps #>
+  register_config_bool Thm.show_tags #>
+  register_config_bool Pattern.unify_trace_failure #>
+  register_config_int Unify.trace_bound #>
+  register_config_int Unify.search_bound #>
+  register_config_bool Unify.trace_simp #>
+  register_config_bool Unify.trace_types #>
+  register_config_int Raw_Simplifier.simp_depth_limit #>
+  register_config_int Raw_Simplifier.simp_trace_depth_limit #>
+  register_config_bool Raw_Simplifier.simp_debug #>
+  register_config_bool Raw_Simplifier.simp_trace #>
+  register_config_bool Local_Defs.unfold_abs_def);
 
 
 (* internal source *)
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Isar/local_defs.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -23,7 +23,6 @@
   val meta_rewrite_conv: Proof.context -> conv
   val meta_rewrite_rule: Proof.context -> thm -> thm
   val abs_def_rule: Proof.context -> thm -> thm
-  val unfold_abs_def_raw: Config.raw
   val unfold_abs_def: bool Config.T
   val unfold: Proof.context -> thm list -> thm -> thm
   val unfold_goals: Proof.context -> thm list -> thm -> thm
@@ -207,8 +206,7 @@
 
 (* unfold object-level rules *)
 
-val unfold_abs_def_raw = Config.declare ("unfold_abs_def", \<^here>) (K (Config.Bool true));
-val unfold_abs_def = Config.bool unfold_abs_def_raw;
+val unfold_abs_def = Config.declare_bool ("unfold_abs_def", \<^here>) (K true);
 
 local
 
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Isar/method.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -495,7 +495,7 @@
     val _ = Seq.pull (method ctxt' src' ctxt' [] (ctxt', Goal.protect 0 Drule.dummy_thm));
   in map Token.closure src' end;
 
-val closure = Config.bool (Config.declare ("Method.closure", \<^here>) (K (Config.Bool true)));
+val closure = Config.declare_bool ("Method.closure", \<^here>) (K true);
 
 fun method_cmd ctxt =
   check_src ctxt #>
@@ -605,8 +605,7 @@
 
 (* sections *)
 
-val old_section_parser =
-  Config.bool (Config.declare ("Method.old_section_parser", \<^here>) (K (Config.Bool false)));
+val old_section_parser = Config.declare_bool ("Method.old_section_parser", \<^here>) (K false);
 
 local
 
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -174,8 +174,7 @@
 
 (* parse commands *)
 
-val bootstrap =
-  Config.bool (Config.declare ("Outer_Syntax.bootstrap", \<^here>) (K (Config.Bool true)));
+val bootstrap = Config.declare_bool ("Outer_Syntax.bootstrap", \<^here>) (K true);
 
 local
 
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -93,7 +93,6 @@
   val read_term_pattern: Proof.context -> string -> term
   val read_term_schematic: Proof.context -> string -> term
   val read_term_abbrev: Proof.context -> string -> term
-  val show_abbrevs_raw: Config.raw
   val show_abbrevs: bool Config.T
   val expand_abbrevs: Proof.context -> term -> term
   val cert_term: Proof.context -> term -> term
@@ -633,8 +632,7 @@
 
 end;
 
-val show_abbrevs_raw = Config.declare ("show_abbrevs", \<^here>) (fn _ => Config.Bool true);
-val show_abbrevs = Config.bool show_abbrevs_raw;
+val show_abbrevs = Config.declare_bool ("show_abbrevs", \<^here>) (K true);
 
 fun contract_abbrevs ctxt t =
   let
@@ -666,8 +664,7 @@
 
 local
 
-val dummies =
-  Config.bool (Config.declare ("Proof_Context.dummies", \<^here>) (K (Config.Bool false)));
+val dummies = Config.declare_bool ("Proof_Context.dummies", \<^here>) (K false);
 
 fun check_dummies ctxt t =
   if Config.get ctxt dummies then t
@@ -978,8 +975,7 @@
 
 (* retrieve facts *)
 
-val dynamic_facts_dummy =
-  Config.bool (Config.declare ("dynamic_facts_dummy_", \<^here>) (fn _ => Config.Bool false));
+val dynamic_facts_dummy = Config.declare_bool ("dynamic_facts_dummy_", \<^here>) (K false);
 
 local
 
@@ -1048,9 +1044,7 @@
 
 (* inner statement mode *)
 
-val inner_stmt =
-  Config.bool (Config.declare ("inner_stmt", \<^here>) (K (Config.Bool false)));
-
+val inner_stmt = Config.declare_bool ("inner_stmt", \<^here>) (K false);
 fun is_stmt ctxt = Config.get ctxt inner_stmt;
 val set_stmt = Config.put inner_stmt;
 val restore_stmt = set_stmt o is_stmt;
@@ -1569,11 +1563,8 @@
 
 (* core context *)
 
-val debug =
-  Config.bool (Config.declare ("Proof_Context.debug", \<^here>) (K (Config.Bool false)));
-
-val verbose =
-  Config.bool (Config.declare ("Proof_Context.verbose", \<^here>) (K (Config.Bool false)));
+val debug = Config.declare_bool ("Proof_Context.debug", \<^here>) (K false);
+val verbose = Config.declare_bool ("Proof_Context.verbose", \<^here>) (K false);
 
 fun pretty_ctxt ctxt =
   if not (Config.get ctxt debug) then []
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/ML/ml_env.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -9,11 +9,8 @@
 sig
   val Isabelle: string
   val SML: string
-  val ML_environment_raw: Config.raw
   val ML_environment: string Config.T
-  val ML_read_global_raw: Config.raw
   val ML_read_global: bool Config.T
-  val ML_write_global_raw: Config.raw
   val ML_write_global: bool Config.T
   val inherit: Context.generic list -> Context.generic -> Context.generic
   type operations =
@@ -48,17 +45,13 @@
 val Isabelle = "Isabelle";
 val SML = "SML";
 
-val ML_environment_raw = Config.declare ("ML_environment", \<^here>) (fn _ => Config.String Isabelle);
-val ML_environment = Config.string ML_environment_raw;
+val ML_environment = Config.declare_string ("ML_environment", \<^here>) (K Isabelle);
 
 
 (* global read/write *)
 
-val ML_read_global_raw = Config.declare ("ML_read_global", \<^here>) (fn _ => Config.Bool true);
-val ML_write_global_raw = Config.declare ("ML_write_global", \<^here>) (fn _ => Config.Bool true);
-
-val ML_read_global = Config.bool ML_read_global_raw;
-val ML_write_global = Config.bool ML_write_global_raw;
+val ML_read_global = Config.declare_bool ("ML_read_global", \<^here>) (K true);
+val ML_write_global = Config.declare_bool ("ML_write_global", \<^here>) (K true);
 
 fun read_global context = Config.get_generic context ML_read_global;
 fun write_global context = Config.get_generic context ML_write_global;
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/ML/ml_options.ML
--- a/src/Pure/ML/ml_options.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/ML/ml_options.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -6,15 +6,11 @@
 
 signature ML_OPTIONS =
 sig
-  val source_trace_raw: Config.raw
   val source_trace: bool Config.T
-  val exception_trace_raw: Config.raw
   val exception_trace: bool Config.T
   val exception_trace_enabled: Context.generic option -> bool
-  val exception_debugger_raw: Config.raw
   val exception_debugger: bool Config.T
   val exception_debugger_enabled: Context.generic option -> bool
-  val debugger_raw: Config.raw
   val debugger: bool Config.T
   val debugger_enabled: Context.generic option -> bool
 end;
@@ -24,38 +20,33 @@
 
 (* source trace *)
 
-val source_trace_raw =
-  Config.declare ("ML_source_trace", \<^here>) (fn _ => Config.Bool false);
-val source_trace = Config.bool source_trace_raw;
+val source_trace = Config.declare_bool ("ML_source_trace", \<^here>) (K false);
 
 
 (* exception trace *)
 
-val exception_trace_raw = Config.declare_option ("ML_exception_trace", \<^here>);
-val exception_trace = Config.bool exception_trace_raw;
+val exception_trace = Config.declare_option_bool ("ML_exception_trace", \<^here>);
 
 fun exception_trace_enabled NONE =
-      (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false)
+      (Options.default_bool (Config.name_of exception_trace) handle ERROR _ => false)
   | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace;
 
 
 (* exception debugger *)
 
-val exception_debugger_raw = Config.declare_option ("ML_exception_debugger", \<^here>);
-val exception_debugger = Config.bool exception_debugger_raw;
+val exception_debugger = Config.declare_option_bool ("ML_exception_debugger", \<^here>);
 
 fun exception_debugger_enabled NONE =
-      (Options.default_bool (Config.name_of exception_debugger_raw) handle ERROR _ => false)
+      (Options.default_bool (Config.name_of exception_debugger) handle ERROR _ => false)
   | exception_debugger_enabled (SOME context) = Config.get_generic context exception_debugger;
 
 
 (* debugger *)
 
-val debugger_raw = Config.declare_option ("ML_debugger", \<^here>);
-val debugger = Config.bool debugger_raw;
+val debugger = Config.declare_option_bool ("ML_debugger", \<^here>);
 
 fun debugger_enabled NONE =
-      (Options.default_bool (Config.name_of debugger_raw) handle ERROR _ => false)
+      (Options.default_bool (Config.name_of debugger) handle ERROR _ => false)
   | debugger_enabled (SOME context) = Config.get_generic context debugger;
 
 end;
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/ML/ml_print_depth.ML
--- a/src/Pure/ML/ml_print_depth.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/ML/ml_print_depth.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -7,7 +7,6 @@
 signature ML_PRINT_DEPTH =
 sig
   val set_print_depth: int -> unit
-  val print_depth_raw: Config.raw
   val print_depth: int Config.T
   val get_print_depth: unit -> int
 end;
@@ -17,11 +16,8 @@
 
 val set_print_depth = ML_Print_Depth.set_print_depth;
 
-val print_depth_raw =
-  Config.declare ("ML_print_depth", \<^here>)
-    (fn _ => Config.Int (ML_Print_Depth.get_print_depth ()));
-
-val print_depth = Config.int print_depth_raw;
+val print_depth =
+  Config.declare_int ("ML_print_depth", \<^here>) (fn _ => ML_Print_Depth.get_print_depth ());
 
 fun get_print_depth () =
   (case Context.get_generic_context () of
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -19,8 +19,7 @@
 structure Reconstruct : RECONSTRUCT =
 struct
 
-val quiet_mode =
-  Config.bool (Config.declare ("Reconstruct.quiet_mode", \<^here>) (K (Config.Bool true)));
+val quiet_mode = Config.declare_bool ("Reconstruct.quiet_mode", \<^here>) (K true);
 
 fun message ctxt msg =
   if Config.get ctxt quiet_mode then () else writeln (msg ());
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Syntax/ast.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -21,9 +21,7 @@
   val fold_ast_p: string -> ast list * ast -> ast
   val unfold_ast: string -> ast -> ast list
   val unfold_ast_p: string -> ast -> ast list * ast
-  val trace_raw: Config.raw
   val trace: bool Config.T
-  val stats_raw: Config.raw
   val stats: bool Config.T
   val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast
 end;
@@ -166,11 +164,8 @@
 
 (* normalize *)
 
-val trace_raw = Config.declare ("syntax_ast_trace", \<^here>) (fn _ => Config.Bool false);
-val trace = Config.bool trace_raw;
-
-val stats_raw = Config.declare ("syntax_ast_stats", \<^here>) (fn _ => Config.Bool false);
-val stats = Config.bool stats_raw;
+val trace = Config.declare_bool ("syntax_ast_trace", \<^here>) (K false);
+val stats = Config.declare_bool ("syntax_ast_stats", \<^here>) (K false);
 
 fun message head body =
   Pretty.string_of (Pretty.block [Pretty.str head, Pretty.brk 1, body]);
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Syntax/parser.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -597,8 +597,7 @@
 
 
 (*trigger value for warnings*)
-val branching_level =
-  Config.int (Config.declare ("syntax_branching_level", \<^here>) (fn _ => Config.Int 600));
+val branching_level = Config.declare_int ("syntax_branching_level", \<^here>) (K 600);
 
 (*get all productions of a NT and NTs chained to it which can
   be started by specified token*)
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Syntax/printer.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -18,13 +18,7 @@
 signature PRINTER =
 sig
   include BASIC_PRINTER
-  val show_brackets_raw: Config.raw
-  val show_types_raw: Config.raw
-  val show_sorts_raw: Config.raw
   val show_markup_default: bool Unsynchronized.ref
-  val show_markup_raw: Config.raw
-  val show_structs_raw: Config.raw
-  val show_question_marks_raw: Config.raw
   val show_type_emphasis: bool Config.T
   val type_emphasis: Proof.context -> typ -> bool
   type prtabs
@@ -52,29 +46,14 @@
 
 (** options for printing **)
 
-val show_brackets_raw = Config.declare_option ("show_brackets", \<^here>);
-val show_brackets = Config.bool show_brackets_raw;
-
-val show_types_raw = Config.declare_option ("show_types", \<^here>);
-val show_types = Config.bool show_types_raw;
-
-val show_sorts_raw = Config.declare_option ("show_sorts", \<^here>);
-val show_sorts = Config.bool show_sorts_raw;
-
+val show_brackets = Config.declare_option_bool ("show_brackets", \<^here>);
+val show_types = Config.declare_option_bool ("show_types", \<^here>);
+val show_sorts = Config.declare_option_bool ("show_sorts", \<^here>);
 val show_markup_default = Unsynchronized.ref false;
-val show_markup_raw =
-  Config.declare ("show_markup", \<^here>) (fn _ => Config.Bool (! show_markup_default));
-val show_markup = Config.bool show_markup_raw;
-
-val show_structs_raw =
-  Config.declare ("show_structs", \<^here>) (fn _ => Config.Bool false);
-val show_structs = Config.bool show_structs_raw;
-
-val show_question_marks_raw = Config.declare_option ("show_question_marks", \<^here>);
-val show_question_marks = Config.bool show_question_marks_raw;
-
-val show_type_emphasis =
-  Config.bool (Config.declare ("show_type_emphasis", \<^here>) (fn _ => Config.Bool true));
+val show_markup = Config.declare_bool ("show_markup", \<^here>) (fn _ => ! show_markup_default);
+val show_structs = Config.declare_bool ("show_structs", \<^here>) (K false);
+val show_question_marks = Config.declare_option_bool ("show_question_marks", \<^here>);
+val show_type_emphasis = Config.declare_bool ("show_type_emphasis", \<^here>) (K true);
 
 fun type_emphasis ctxt T =
   T <> dummyT andalso
@@ -223,8 +202,7 @@
   | is_chain [Arg _] = true
   | is_chain _  = false;
 
-val pretty_priority =
-  Config.int (Config.declare ("Syntax.pretty_priority", \<^here>) (K (Config.Int 0)));
+val pretty_priority = Config.declare_int ("Syntax.pretty_priority", \<^here>) (K 0);
 
 fun pretty type_mode curried ctxt tabs trf markup_trans markup_extern ast0 =
   let
diff -r b4ea943ce0b7 -r f77cc54f6d47 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;
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -29,7 +29,6 @@
   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
-  val eta_contract_raw: Config.raw
   val mark_bound_abs: string * typ -> term
   val mark_bound_body: string * typ -> term
   val bound_vars: (string * typ) list -> term -> term
@@ -297,8 +296,7 @@
       | t' => Abs (a, T, t'))
   | eta_abs t = t;
 
-val eta_contract_raw = Config.declare_option ("eta_contract", \<^here>);
-val eta_contract = Config.bool eta_contract_raw;
+val eta_contract = Config.declare_option_bool ("eta_contract", \<^here>);
 
 fun eta_contr ctxt tm =
   if Config.get ctxt eta_contract then eta_abs tm else tm;
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/config.ML
--- a/src/Pure/config.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/config.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -10,11 +10,8 @@
   val print_value: value -> string
   val print_type: value -> string
   type 'a T
-  type raw = value T
-  val bool: raw -> bool T
-  val int: raw -> int T
-  val real: raw -> real T
-  val string: raw -> string T
+  val name_of: 'a T -> string
+  val pos_of: 'a T -> Position.T
   val get: Proof.context -> 'a T -> 'a
   val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
   val put: 'a T -> 'a -> Proof.context -> Proof.context
@@ -27,10 +24,24 @@
   val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
   val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
   val restore_generic: 'a T -> Context.generic -> Context.generic -> Context.generic
-  val declare: string * Position.T -> (Context.generic -> value) -> raw
-  val declare_option: string * Position.T -> raw
-  val name_of: 'a T -> string
-  val pos_of: 'a T -> Position.T
+  val bool: value T -> bool T
+  val bool_value: bool T -> value T
+  val int: value T -> int T
+  val int_value: int T -> value T
+  val real: value T -> real T
+  val real_value: real T -> value T
+  val string: value T -> string T
+  val string_value: string T -> value T
+  val declare: string * Position.T -> (Context.generic -> value) -> value T
+  val declare_bool: string * Position.T -> (Context.generic -> bool) -> bool T
+  val declare_int: string * Position.T -> (Context.generic -> int) -> int T
+  val declare_real: string * Position.T -> (Context.generic -> real) -> real T
+  val declare_string: string * Position.T -> (Context.generic -> string) -> string T
+  val declare_option: string * Position.T -> value T
+  val declare_option_bool: string * Position.T -> bool T
+  val declare_option_int: string * Position.T -> int T
+  val declare_option_real: string * Position.T -> real T
+  val declare_option_string: string * Position.T -> string T
 end;
 
 structure Config: CONFIG =
@@ -78,18 +89,8 @@
   get_value: Context.generic -> 'a,
   map_value: ('a -> 'a) -> Context.generic -> Context.generic};
 
-type raw = value T;
-
-fun coerce make dest (Config {name, pos, get_value, map_value}) = Config
- {name = name,
-  pos = pos,
-  get_value = dest o get_value,
-  map_value = fn f => map_value (make o f o dest)};
-
-val bool = coerce Bool (fn Bool b => b);
-val int = coerce Int (fn Int i => i);
-val real = coerce Real (fn Real x => x);
-val string = coerce String (fn String s => s);
+fun name_of (Config {name, ...}) = name;
+fun pos_of (Config {pos, ...}) = pos;
 
 fun get_generic context (Config {get_value, ...}) = get_value context;
 fun map_generic (Config {map_value, ...}) f context = map_value f context;
@@ -107,7 +108,23 @@
 fun restore_global config thy = put_global config (get_global thy config);
 
 
-(* context information *)
+(* coerce type *)
+
+fun coerce make dest (Config {name, pos, get_value, map_value}) = Config
+ {name = name,
+  pos = pos,
+  get_value = dest o get_value,
+  map_value = fn f => map_value (make o f o dest)};
+
+fun coerce_pair make dest = (coerce make dest, coerce dest make);
+
+val (bool, bool_value) = coerce_pair Bool (fn Bool b => b);
+val (int, int_value) = coerce_pair Int (fn Int i => i);
+val (real, real_value) = coerce_pair Real (fn Real x => x);
+val (string, string_value) = coerce_pair String (fn String s => s);
+
+
+(* context data *)
 
 structure Data = Generic_Data
 (
@@ -132,6 +149,14 @@
     Config {name = name, pos = pos, get_value = get_value, map_value = map_value}
   end;
 
+fun declare_bool name default = bool (declare name (Bool o default));
+fun declare_int name default = int (declare name (Int o default));
+fun declare_real name default = real (declare name (Real o default));
+fun declare_string name default = string (declare name (String o default));
+
+
+(* system options *)
+
 fun declare_option (name, pos) =
   let
     val typ = Options.default_typ name;
@@ -143,9 +168,10 @@
       else error ("Unknown type for option " ^ quote name ^ Position.here pos ^ " : " ^ quote typ);
   in declare (name, pos) default end;
 
-fun name_of (Config {name, ...}) = name;
-fun pos_of (Config {pos, ...}) = pos;
-
+val declare_option_bool = bool o declare_option;
+val declare_option_int = int o declare_option;
+val declare_option_real = real o declare_option;
+val declare_option_string = string o declare_option;
 
 (*final declarations of this structure!*)
 val get = get_ctxt;
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/goal.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -36,7 +36,6 @@
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val prove_global: theory -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
-  val quick_and_dirty_raw: Config.raw
   val prove_sorry: Proof.context -> string list -> term list -> term ->
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
   val prove_sorry_global: theory -> string list -> term list -> term ->
@@ -242,8 +241,7 @@
 
 (* skip proofs *)
 
-val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", \<^here>);
-val quick_and_dirty = Config.bool quick_and_dirty_raw;
+val quick_and_dirty = Config.declare_option_bool ("quick_and_dirty", \<^here>);
 
 fun prove_sorry ctxt xs asms prop tac =
   if Config.get ctxt quick_and_dirty then
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/goal_display.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -7,9 +7,7 @@
 
 signature GOAL_DISPLAY =
 sig
-  val goals_limit_raw: Config.raw
   val goals_limit: int Config.T
-  val show_main_goal_raw: Config.raw
   val show_main_goal: bool Config.T
   val pretty_goals: Proof.context -> thm -> Pretty.T list
   val pretty_goal: Proof.context -> thm -> Pretty.T
@@ -19,11 +17,8 @@
 structure Goal_Display: GOAL_DISPLAY =
 struct
 
-val goals_limit_raw = Config.declare_option ("goals_limit", \<^here>);
-val goals_limit = Config.int goals_limit_raw;
-
-val show_main_goal_raw = Config.declare_option ("show_main_goal", \<^here>);
-val show_main_goal = Config.bool show_main_goal_raw;
+val goals_limit = Config.declare_option_int ("goals_limit", \<^here>);
+val show_main_goal = Config.declare_option_bool ("show_main_goal", \<^here>);
 
 
 (*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/more_thm.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -115,11 +115,8 @@
   val kind: string -> attribute
   val register_proofs: thm list lazy -> theory -> theory
   val consolidate_theory: theory -> unit
-  val show_consts_raw: Config.raw
   val show_consts: bool Config.T
-  val show_hyps_raw: Config.raw
   val show_hyps: bool Config.T
-  val show_tags_raw: Config.raw
   val show_tags: bool Config.T
   val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T
@@ -686,14 +683,9 @@
 
 (* options *)
 
-val show_consts_raw = Config.declare_option ("show_consts", \<^here>);
-val show_consts = Config.bool show_consts_raw;
-
-val show_hyps_raw = Config.declare ("show_hyps", \<^here>) (fn _ => Config.Bool false);
-val show_hyps = Config.bool show_hyps_raw;
-
-val show_tags_raw = Config.declare ("show_tags", \<^here>) (fn _ => Config.Bool false);
-val show_tags = Config.bool show_tags_raw;
+val show_consts = Config.declare_option_bool ("show_consts", \<^here>);
+val show_hyps = Config.declare_bool ("show_hyps", \<^here>) (K false);
+val show_tags = Config.declare_bool ("show_tags", \<^here>) (K false);
 
 
 (* pretty_thm etc. *)
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/pattern.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -14,7 +14,6 @@
 sig
   exception Unif
   exception Pattern
-  val unify_trace_failure_raw: Config.raw
   val unify_trace_failure: bool Config.T
   val unify_types: Context.generic -> typ * typ -> Envir.env -> Envir.env
   val unify: Context.generic -> term * term -> Envir.env -> Envir.env
@@ -30,9 +29,7 @@
 exception Unif;
 exception Pattern;
 
-val unify_trace_failure_raw =
-  Config.declare ("unify_trace_failure", \<^here>) (fn _ => Config.Bool false);
-val unify_trace_failure = Config.bool unify_trace_failure_raw;
+val unify_trace_failure = Config.declare_bool ("unify_trace_failure", \<^here>) (K false);
 
 fun string_of_term ctxt env binders t =
   Syntax.string_of_term ctxt (Envir.norm_term env (subst_bounds (map Free binders, t)));
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/raw_simplifier.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -104,11 +104,7 @@
   val set_term_ord: (term * term -> order) -> Proof.context -> Proof.context
   val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context
   val solver: Proof.context -> solver -> int -> tactic
-  val simp_depth_limit_raw: Config.raw
   val default_mk_sym: Proof.context -> thm -> thm option
-  val simp_trace_depth_limit_raw: Config.raw
-  val simp_trace_raw: Config.raw
-  val simp_debug_raw: Config.raw
   val add_prems: thm list -> Proof.context -> Proof.context
   val set_reorient: (Proof.context -> term list -> term -> term -> bool) ->
     Proof.context -> Proof.context
@@ -396,12 +392,8 @@
 As of 2017, 25 would suffice; 40 builds in a safety margin.
 *)
 
-val simp_depth_limit_raw = Config.declare ("simp_depth_limit", \<^here>) (K (Config.Int 40));
-val simp_depth_limit = Config.int simp_depth_limit_raw;
-
-val simp_trace_depth_limit_raw =
-  Config.declare ("simp_trace_depth_limit", \<^here>) (fn _ => Config.Int 1);
-val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw;
+val simp_depth_limit = Config.declare_int ("simp_depth_limit", \<^here>) (K 40);
+val simp_trace_depth_limit = Config.declare_int ("simp_trace_depth_limit", \<^here>) (K 1);
 
 fun inc_simp_depth ctxt =
   ctxt |> map_simpset1 (fn (rules, prems, (depth, exceeded)) =>
@@ -419,11 +411,8 @@
 
 exception SIMPLIFIER of string * thm list;
 
-val simp_debug_raw = Config.declare ("simp_debug", \<^here>) (K (Config.Bool false));
-val simp_debug = Config.bool simp_debug_raw;
-
-val simp_trace_raw = Config.declare ("simp_trace", \<^here>) (fn _ => Config.Bool false);
-val simp_trace = Config.bool simp_trace_raw;
+val simp_debug = Config.declare_bool ("simp_debug", \<^here>) (K false);
+val simp_trace = Config.declare_bool ("simp_trace", \<^here>) (K false);
 
 fun cond_warning ctxt msg =
   if Context_Position.is_really_visible ctxt then warning (msg ()) else ();
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/type_infer.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -100,8 +100,7 @@
 
 (* fixate -- introduce fresh type variables *)
 
-val object_logic =
-  Config.bool (Config.declare ("Type_Infer.object_logic", \<^here>) (K (Config.Bool true)));
+val object_logic = Config.declare_bool ("Type_Infer.object_logic", \<^here>) (K true);
 
 fun fixate ctxt pattern ts =
   let
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/type_infer_context.ML
--- a/src/Pure/type_infer_context.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/type_infer_context.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -20,8 +20,7 @@
 
 (* constraints *)
 
-val const_sorts =
-  Config.bool (Config.declare ("const_sorts", \<^here>) (K (Config.Bool true)));
+val const_sorts = Config.declare_bool ("const_sorts", \<^here>) (K true);
 
 fun const_type ctxt =
   try ((not (Config.get ctxt const_sorts) ? Type.strip_sorts) o
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/unify.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -11,13 +11,9 @@
 
 signature UNIFY =
 sig
-  val trace_bound_raw: Config.raw
   val trace_bound: int Config.T
-  val search_bound_raw: Config.raw
   val search_bound: int Config.T
-  val trace_simp_raw: Config.raw
   val trace_simp: bool Config.T
-  val trace_types_raw: Config.raw
   val trace_types: bool Config.T
   val hounifiers: Context.generic * Envir.env * ((term * term) list) ->
     (Envir.env * (term * term) list) Seq.seq
@@ -32,20 +28,16 @@
 (*Unification options*)
 
 (*tracing starts above this depth, 0 for full*)
-val trace_bound_raw = Config.declare ("unify_trace_bound", \<^here>) (K (Config.Int 50));
-val trace_bound = Config.int trace_bound_raw;
+val trace_bound = Config.declare_int ("unify_trace_bound", \<^here>) (K 50);
 
 (*unification quits above this depth*)
-val search_bound_raw = Config.declare ("unify_search_bound", \<^here>) (K (Config.Int 60));
-val search_bound = Config.int search_bound_raw;
+val search_bound = Config.declare_int ("unify_search_bound", \<^here>) (K 60);
 
 (*print dpairs before calling SIMPL*)
-val trace_simp_raw = Config.declare ("unify_trace_simp", \<^here>) (K (Config.Bool false));
-val trace_simp = Config.bool trace_simp_raw;
+val trace_simp = Config.declare_bool ("unify_trace_simp", \<^here>) (K false);
 
 (*announce potential incompleteness of type unification*)
-val trace_types_raw = Config.declare ("unify_trace_types", \<^here>) (K (Config.Bool false));
-val trace_types = Config.bool trace_types_raw;
+val trace_types = Config.declare_bool ("unify_trace_types", \<^here>) (K false);
 
 
 type binderlist = (string * typ) list;
diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/variable.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -334,9 +334,7 @@
 
 (* inner body mode *)
 
-val inner_body =
-  Config.bool (Config.declare ("inner_body", \<^here>) (K (Config.Bool false)));
-
+val inner_body = Config.declare_bool ("inner_body", \<^here>) (K false);
 fun is_body ctxt = Config.get ctxt inner_body;
 val set_body = Config.put inner_body;
 fun restore_body ctxt = set_body (is_body ctxt);
@@ -344,9 +342,7 @@
 
 (* proper mode *)
 
-val proper_fixes =
-  Config.bool (Config.declare ("proper_fixes", \<^here>) (K (Config.Bool true)));
-
+val proper_fixes = Config.declare_bool ("proper_fixes", \<^here>) (K true);
 val improper_fixes = Config.put proper_fixes false;
 fun restore_proper_fixes ctxt = Config.put proper_fixes (Config.get ctxt proper_fixes);
 
@@ -644,9 +640,7 @@
 
 (* focus on outermost parameters: \<And>x y z. B *)
 
-val bound_focus =
-  Config.bool (Config.declare ("bound_focus", \<^here>) (K (Config.Bool false)));
-
+val bound_focus = Config.declare_bool ("bound_focus", \<^here>) (K false);
 fun is_bound_focus ctxt = Config.get ctxt bound_focus;
 val set_bound_focus = Config.put bound_focus;
 fun restore_bound_focus ctxt = set_bound_focus (is_bound_focus ctxt);