more source positions;
authorwenzelm
Sun Apr 06 16:36:28 2014 +0200 (2014-04-06)
changeset 564387f6b2634d853
parent 56437 b14bd153a753
child 56439 95e2656b3b23
more source positions;
src/Pure/General/name_space.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/proof_context.ML
src/Pure/ML/ml_options.ML
src/Pure/ROOT.ML
src/Pure/Syntax/ast.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_trans.ML
src/Pure/Thy/thy_output.ML
src/Pure/config.ML
src/Pure/display.ML
src/Pure/goal_display.ML
src/Pure/pattern.ML
src/Pure/raw_simplifier.ML
src/Pure/skip_proof.ML
src/Pure/type_infer_context.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/General/name_space.ML	Sun Apr 06 15:51:02 2014 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Sun Apr 06 16:36:28 2014 +0200
     1.3 @@ -189,13 +189,13 @@
     1.4  
     1.5  (* extern *)
     1.6  
     1.7 -val names_long_raw = Config.declare_option "names_long";
     1.8 +val names_long_raw = Config.declare_option ("names_long", @{here});
     1.9  val names_long = Config.bool names_long_raw;
    1.10  
    1.11 -val names_short_raw = Config.declare_option "names_short";
    1.12 +val names_short_raw = Config.declare_option ("names_short", @{here});
    1.13  val names_short = Config.bool names_short_raw;
    1.14  
    1.15 -val names_unique_raw = Config.declare_option "names_unique";
    1.16 +val names_unique_raw = Config.declare_option ("names_unique", @{here});
    1.17  val names_unique = Config.bool names_unique_raw;
    1.18  
    1.19  fun extern ctxt space name =
     2.1 --- a/src/Pure/Isar/attrib.ML	Sun Apr 06 15:51:02 2014 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Sun Apr 06 16:36:28 2014 +0200
     2.3 @@ -58,14 +58,14 @@
     2.4    val setup_config_int: Binding.binding -> (Context.generic -> int) -> int Config.T
     2.5    val setup_config_real: Binding.binding -> (Context.generic -> real) -> real Config.T
     2.6    val setup_config_string: Binding.binding -> (Context.generic -> string) -> string Config.T
     2.7 -  val option_bool: string -> bool Config.T * (theory -> theory)
     2.8 -  val option_int: string -> int Config.T * (theory -> theory)
     2.9 -  val option_real: string -> real Config.T * (theory -> theory)
    2.10 -  val option_string: string -> string Config.T * (theory -> theory)
    2.11 -  val setup_option_bool: string -> bool Config.T
    2.12 -  val setup_option_int: string -> int Config.T
    2.13 -  val setup_option_real: string -> real Config.T
    2.14 -  val setup_option_string: string -> string Config.T
    2.15 +  val option_bool: string * Position.T -> bool Config.T * (theory -> theory)
    2.16 +  val option_int: string * Position.T -> int Config.T * (theory -> theory)
    2.17 +  val option_real: string * Position.T -> real Config.T * (theory -> theory)
    2.18 +  val option_string: string * Position.T -> string Config.T * (theory -> theory)
    2.19 +  val setup_option_bool: string * Position.T -> bool Config.T
    2.20 +  val setup_option_int: string * Position.T -> int Config.T
    2.21 +  val setup_option_real: string * Position.T -> real Config.T
    2.22 +  val setup_option_string: string * Position.T -> string Config.T
    2.23  end;
    2.24  
    2.25  structure Attrib: ATTRIB =
    2.26 @@ -374,13 +374,15 @@
    2.27  fun declare make coerce binding default =
    2.28    let
    2.29      val name = Binding.name_of binding;
    2.30 -    val config_value = Config.declare name (make o default);
    2.31 +    val pos = Binding.pos_of binding;
    2.32 +    val config_value = Config.declare (name, pos) (make o default);
    2.33      val config = coerce config_value;
    2.34    in (config, register binding config_value) end;
    2.35  
    2.36  in
    2.37  
    2.38 -fun register_config config = register (Binding.name (Config.name_of config)) config;
    2.39 +fun register_config config =
    2.40 +  register (Binding.make (Config.name_of config, Config.pos_of config)) config;
    2.41  
    2.42  val config_bool = declare Config.Bool Config.bool;
    2.43  val config_int = declare Config.Int Config.int;
    2.44 @@ -414,14 +416,14 @@
    2.45  
    2.46  local
    2.47  
    2.48 -fun declare_option coerce name =
    2.49 +fun declare_option coerce (name, pos) =
    2.50    let
    2.51 -    val config = Config.declare_option name;
    2.52 +    val config = Config.declare_option (name, pos);
    2.53    in (coerce config, register_config config) end;
    2.54  
    2.55 -fun setup_option coerce name =
    2.56 +fun setup_option coerce (name, pos) =
    2.57    let
    2.58 -    val config = Config.declare_option name;
    2.59 +    val config = Config.declare_option (name, pos);
    2.60      val _ = Theory.setup (register_config config);
    2.61    in coerce config end;
    2.62  
     3.1 --- a/src/Pure/Isar/proof_context.ML	Sun Apr 06 15:51:02 2014 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Apr 06 16:36:28 2014 +0200
     3.3 @@ -572,7 +572,7 @@
     3.4  
     3.5  end;
     3.6  
     3.7 -val show_abbrevs_raw = Config.declare "show_abbrevs" (fn _ => Config.Bool true);
     3.8 +val show_abbrevs_raw = Config.declare ("show_abbrevs", @{here}) (fn _ => Config.Bool true);
     3.9  val show_abbrevs = Config.bool show_abbrevs_raw;
    3.10  
    3.11  fun contract_abbrevs ctxt t =
    3.12 @@ -605,7 +605,8 @@
    3.13  
    3.14  local
    3.15  
    3.16 -val dummies = Config.bool (Config.declare "Proof_Context.dummies" (K (Config.Bool false)));
    3.17 +val dummies =
    3.18 +  Config.bool (Config.declare ("Proof_Context.dummies", @{here}) (K (Config.Bool false)));
    3.19  
    3.20  fun check_dummies ctxt t =
    3.21    if Config.get ctxt dummies then t
    3.22 @@ -1338,8 +1339,11 @@
    3.23  
    3.24  (* core context *)
    3.25  
    3.26 -val debug = Config.bool (Config.declare "Proof_Context.debug" (K (Config.Bool false)));
    3.27 -val verbose = Config.bool (Config.declare "Proof_Context.verbose" (K (Config.Bool false)));
    3.28 +val debug =
    3.29 +  Config.bool (Config.declare ("Proof_Context.debug", @{here}) (K (Config.Bool false)));
    3.30 +
    3.31 +val verbose =
    3.32 +  Config.bool (Config.declare ("Proof_Context.verbose", @{here}) (K (Config.Bool false)));
    3.33  
    3.34  fun pretty_ctxt ctxt =
    3.35    if not (Config.get ctxt debug) then []
     4.1 --- a/src/Pure/ML/ml_options.ML	Sun Apr 06 15:51:02 2014 +0200
     4.2 +++ b/src/Pure/ML/ml_options.ML	Sun Apr 06 16:36:28 2014 +0200
     4.3 @@ -21,13 +21,14 @@
     4.4  
     4.5  (* source trace *)
     4.6  
     4.7 -val source_trace_raw = Config.declare "ML_source_trace" (fn _ => Config.Bool false);
     4.8 +val source_trace_raw =
     4.9 +  Config.declare ("ML_source_trace", @{here}) (fn _ => Config.Bool false);
    4.10  val source_trace = Config.bool source_trace_raw;
    4.11  
    4.12  
    4.13  (* exception trace *)
    4.14  
    4.15 -val exception_trace_raw = Config.declare_option "ML_exception_trace";
    4.16 +val exception_trace_raw = Config.declare_option ("ML_exception_trace", @{here});
    4.17  val exception_trace = Config.bool exception_trace_raw;
    4.18  
    4.19  fun exception_trace_enabled NONE =
    4.20 @@ -38,7 +39,7 @@
    4.21  (* print depth *)
    4.22  
    4.23  val print_depth_raw =
    4.24 -  Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ()));
    4.25 +  Config.declare ("ML_print_depth", @{here}) (fn _ => Config.Int (get_default_print_depth ()));
    4.26  val print_depth = Config.int print_depth_raw;
    4.27  
    4.28  fun get_print_depth () =
     5.1 --- a/src/Pure/ROOT.ML	Sun Apr 06 15:51:02 2014 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Sun Apr 06 16:36:28 2014 +0200
     5.3 @@ -141,9 +141,6 @@
     5.4  use "context_position.ML";
     5.5  use "config.ML";
     5.6  
     5.7 -val quick_and_dirty_raw = Config.declare_option "quick_and_dirty";
     5.8 -val quick_and_dirty = Config.bool quick_and_dirty_raw;
     5.9 -
    5.10  
    5.11  (* inner syntax *)
    5.12  
     6.1 --- a/src/Pure/Syntax/ast.ML	Sun Apr 06 15:51:02 2014 +0200
     6.2 +++ b/src/Pure/Syntax/ast.ML	Sun Apr 06 16:36:28 2014 +0200
     6.3 @@ -164,10 +164,10 @@
     6.4  
     6.5  (* normalize *)
     6.6  
     6.7 -val trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false);
     6.8 +val trace_raw = Config.declare ("syntax_ast_trace", @{here}) (fn _ => Config.Bool false);
     6.9  val trace = Config.bool trace_raw;
    6.10  
    6.11 -val stats_raw = Config.declare "syntax_ast_stats" (fn _ => Config.Bool false);
    6.12 +val stats_raw = Config.declare ("syntax_ast_stats", @{here}) (fn _ => Config.Bool false);
    6.13  val stats = Config.bool stats_raw;
    6.14  
    6.15  fun message head body =
     7.1 --- a/src/Pure/Syntax/parser.ML	Sun Apr 06 15:51:02 2014 +0200
     7.2 +++ b/src/Pure/Syntax/parser.ML	Sun Apr 06 16:36:28 2014 +0200
     7.3 @@ -626,7 +626,8 @@
     7.4  
     7.5  
     7.6  (*trigger value for warnings*)
     7.7 -val branching_level = Config.int (Config.declare "syntax_branching_level" (fn _ => Config.Int 600));
     7.8 +val branching_level =
     7.9 +  Config.int (Config.declare ("syntax_branching_level", @{here}) (fn _ => Config.Int 600));
    7.10  
    7.11  (*get all productions of a NT and NTs chained to it which can
    7.12    be started by specified token*)
     8.1 --- a/src/Pure/Syntax/printer.ML	Sun Apr 06 15:51:02 2014 +0200
     8.2 +++ b/src/Pure/Syntax/printer.ML	Sun Apr 06 16:36:28 2014 +0200
     8.3 @@ -48,27 +48,29 @@
     8.4  
     8.5  (** options for printing **)
     8.6  
     8.7 -val show_brackets_raw = Config.declare_option "show_brackets";
     8.8 +val show_brackets_raw = Config.declare_option ("show_brackets", @{here});
     8.9  val show_brackets = Config.bool show_brackets_raw;
    8.10  
    8.11 -val show_types_raw = Config.declare_option "show_types";
    8.12 +val show_types_raw = Config.declare_option ("show_types", @{here});
    8.13  val show_types = Config.bool show_types_raw;
    8.14  
    8.15 -val show_sorts_raw = Config.declare_option "show_sorts";
    8.16 +val show_sorts_raw = Config.declare_option ("show_sorts", @{here});
    8.17  val show_sorts = Config.bool show_sorts_raw;
    8.18  
    8.19  val show_markup_default = Unsynchronized.ref false;
    8.20 -val show_markup_raw = Config.declare "show_markup" (fn _ => Config.Bool (! show_markup_default));
    8.21 +val show_markup_raw =
    8.22 +  Config.declare ("show_markup", @{here}) (fn _ => Config.Bool (! show_markup_default));
    8.23  val show_markup = Config.bool show_markup_raw;
    8.24  
    8.25 -val show_structs_raw = Config.declare "show_structs" (fn _ => Config.Bool false);
    8.26 +val show_structs_raw =
    8.27 +  Config.declare ("show_structs", @{here}) (fn _ => Config.Bool false);
    8.28  val show_structs = Config.bool show_structs_raw;
    8.29  
    8.30 -val show_question_marks_raw = Config.declare_option "show_question_marks";
    8.31 +val show_question_marks_raw = Config.declare_option ("show_question_marks", @{here});
    8.32  val show_question_marks = Config.bool show_question_marks_raw;
    8.33  
    8.34  val show_type_emphasis =
    8.35 -  Config.bool (Config.declare "show_type_emphasis" (fn _ => Config.Bool true));
    8.36 +  Config.bool (Config.declare ("show_type_emphasis", @{here}) (fn _ => Config.Bool true));
    8.37  
    8.38  fun type_emphasis ctxt T =
    8.39    T <> dummyT andalso
    8.40 @@ -166,7 +168,8 @@
    8.41    | is_chain [Arg _] = true
    8.42    | is_chain _  = false;
    8.43  
    8.44 -val pretty_priority = Config.int (Config.declare "Syntax.pretty_priority" (K (Config.Int 0)));
    8.45 +val pretty_priority =
    8.46 +  Config.int (Config.declare ("Syntax.pretty_priority", @{here}) (K (Config.Int 0)));
    8.47  
    8.48  fun pretty type_mode curried ctxt tabs trf markup_trans markup_extern ast0 =
    8.49    let
     9.1 --- a/src/Pure/Syntax/syntax.ML	Sun Apr 06 15:51:02 2014 +0200
     9.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Apr 06 16:36:28 2014 +0200
     9.3 @@ -148,12 +148,14 @@
     9.4  
     9.5  (* configuration options *)
     9.6  
     9.7 -val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
     9.8 +val root = Config.string (Config.declare ("syntax_root", @{here}) (K (Config.String "any")));
     9.9  
    9.10 -val ambiguity_warning_raw = Config.declare "syntax_ambiguity_warning" (fn _ => Config.Bool true);
    9.11 +val ambiguity_warning_raw =
    9.12 +  Config.declare ("syntax_ambiguity_warning", @{here}) (fn _ => Config.Bool true);
    9.13  val ambiguity_warning = Config.bool ambiguity_warning_raw;
    9.14  
    9.15 -val ambiguity_limit_raw = Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10);
    9.16 +val ambiguity_limit_raw =
    9.17 +  Config.declare ("syntax_ambiguity_limit", @{here}) (fn _ => Config.Int 10);
    9.18  val ambiguity_limit = Config.int ambiguity_limit_raw;
    9.19  
    9.20  
    9.21 @@ -305,7 +307,8 @@
    9.22  
    9.23  (* global pretty printing *)
    9.24  
    9.25 -val pretty_global = Config.bool (Config.declare "Syntax.pretty_global" (K (Config.Bool false)));
    9.26 +val pretty_global =
    9.27 +  Config.bool (Config.declare ("Syntax.pretty_global", @{here}) (K (Config.Bool false)));
    9.28  fun is_pretty_global ctxt = Config.get ctxt pretty_global;
    9.29  val set_pretty_global = Config.put pretty_global;
    9.30  val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
    10.1 --- a/src/Pure/Syntax/syntax_trans.ML	Sun Apr 06 15:51:02 2014 +0200
    10.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Sun Apr 06 16:36:28 2014 +0200
    10.3 @@ -295,7 +295,7 @@
    10.4        | t' => Abs (a, T, t'))
    10.5    | eta_abs t = t;
    10.6  
    10.7 -val eta_contract_raw = Config.declare_option "eta_contract";
    10.8 +val eta_contract_raw = Config.declare_option ("eta_contract", @{here});
    10.9  val eta_contract = Config.bool eta_contract_raw;
   10.10  
   10.11  fun eta_contr ctxt tm =
    11.1 --- a/src/Pure/Thy/thy_output.ML	Sun Apr 06 15:51:02 2014 +0200
    11.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Apr 06 16:36:28 2014 +0200
    11.3 @@ -43,12 +43,12 @@
    11.4  
    11.5  (** options **)
    11.6  
    11.7 -val display = Attrib.setup_option_bool "thy_output_display";
    11.8 -val break = Attrib.setup_option_bool "thy_output_break";
    11.9 -val quotes = Attrib.setup_option_bool "thy_output_quotes";
   11.10 -val indent = Attrib.setup_option_int "thy_output_indent";
   11.11 -val source = Attrib.setup_option_bool "thy_output_source";
   11.12 -val modes = Attrib.setup_option_string "thy_output_modes";
   11.13 +val display = Attrib.setup_option_bool ("thy_output_display", @{here});
   11.14 +val break = Attrib.setup_option_bool ("thy_output_break", @{here});
   11.15 +val quotes = Attrib.setup_option_bool ("thy_output_quotes", @{here});
   11.16 +val indent = Attrib.setup_option_int ("thy_output_indent", @{here});
   11.17 +val source = Attrib.setup_option_bool ("thy_output_source", @{here});
   11.18 +val modes = Attrib.setup_option_string ("thy_output_modes", @{here});
   11.19  
   11.20  
   11.21  structure Wrappers = Proof_Data
    12.1 --- a/src/Pure/config.ML	Sun Apr 06 15:51:02 2014 +0200
    12.2 +++ b/src/Pure/config.ML	Sun Apr 06 16:36:28 2014 +0200
    12.3 @@ -24,11 +24,12 @@
    12.4    val get_generic: Context.generic -> 'a T -> 'a
    12.5    val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
    12.6    val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
    12.7 -  val declare: string -> (Context.generic -> value) -> raw
    12.8 -  val declare_global: string -> (Context.generic -> value) -> raw
    12.9 -  val declare_option: string -> raw
   12.10 -  val declare_option_global: string -> raw
   12.11 +  val declare: string * Position.T -> (Context.generic -> value) -> raw
   12.12 +  val declare_global: string * Position.T -> (Context.generic -> value) -> raw
   12.13 +  val declare_option: string * Position.T -> raw
   12.14 +  val declare_option_global: string * Position.T -> raw
   12.15    val name_of: 'a T -> string
   12.16 +  val pos_of: 'a T -> Position.T
   12.17  end;
   12.18  
   12.19  structure Config: CONFIG =
   12.20 @@ -59,11 +60,11 @@
   12.21    | same_type (String _) (String _) = true
   12.22    | same_type _ _ = false;
   12.23  
   12.24 -fun type_check name f value =
   12.25 +fun type_check (name, pos) f value =
   12.26    let
   12.27      val value' = f value;
   12.28      val _ = same_type value value' orelse
   12.29 -      error ("Ill-typed configuration option " ^ quote name ^ ": " ^
   12.30 +      error ("Ill-typed configuration option " ^ quote name ^ Position.here pos ^ ": " ^
   12.31          print_type value ^ " expected,\nbut " ^ print_type value' ^ " was found");
   12.32    in value' end;
   12.33  
   12.34 @@ -72,13 +73,15 @@
   12.35  
   12.36  datatype 'a T = Config of
   12.37   {name: string,
   12.38 +  pos: Position.T,
   12.39    get_value: Context.generic -> 'a,
   12.40    map_value: ('a -> 'a) -> Context.generic -> Context.generic};
   12.41  
   12.42  type raw = value T;
   12.43  
   12.44 -fun coerce make dest (Config {name, get_value, map_value}) = Config
   12.45 +fun coerce make dest (Config {name, pos, get_value, map_value}) = Config
   12.46   {name = name,
   12.47 +  pos = pos,
   12.48    get_value = dest o get_value,
   12.49    map_value = fn f => map_value (make o f o dest)};
   12.50  
   12.51 @@ -112,7 +115,7 @@
   12.52  
   12.53  local
   12.54  
   12.55 -fun declare_generic global name default =
   12.56 +fun declare_generic global (name, pos) default =
   12.57    let
   12.58      val id = serial ();
   12.59  
   12.60 @@ -122,7 +125,7 @@
   12.61        | NONE => default context);
   12.62  
   12.63      fun update_value f context =
   12.64 -      Value.map (Inttab.update (id, type_check name f (get_value context))) context;
   12.65 +      Value.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context;
   12.66  
   12.67      fun map_value f (context as Context.Proof ctxt) =
   12.68            let val context' = update_value f context in
   12.69 @@ -137,9 +140,9 @@
   12.70              else context'
   12.71            end
   12.72        | map_value f context = update_value f context;
   12.73 -  in Config {name = name, get_value = get_value, map_value = map_value} end;
   12.74 +  in Config {name = name, pos = pos, get_value = get_value, map_value = map_value} end;
   12.75  
   12.76 -fun declare_option_generic global name =
   12.77 +fun declare_option_generic global (name, pos) =
   12.78    let
   12.79      val typ = Options.default_typ name;
   12.80      val default =
   12.81 @@ -147,8 +150,8 @@
   12.82        else if typ = Options.intT then fn _ => Int (Options.default_int name)
   12.83        else if typ = Options.realT then fn _ => Real (Options.default_real name)
   12.84        else if typ = Options.stringT then fn _ => String (Options.default_string name)
   12.85 -      else error ("Unknown type for option " ^ quote name ^ " : " ^ quote typ);
   12.86 -  in declare_generic global name default end;
   12.87 +      else error ("Unknown type for option " ^ quote name ^ Position.here pos ^ " : " ^ quote typ);
   12.88 +  in declare_generic global (name, pos) default end;
   12.89  
   12.90  in
   12.91  
   12.92 @@ -160,6 +163,7 @@
   12.93  end;
   12.94  
   12.95  fun name_of (Config {name, ...}) = name;
   12.96 +fun pos_of (Config {pos, ...}) = pos;
   12.97  
   12.98  
   12.99  (*final declarations of this structure!*)
    13.1 --- a/src/Pure/display.ML	Sun Apr 06 15:51:02 2014 +0200
    13.2 +++ b/src/Pure/display.ML	Sun Apr 06 16:36:28 2014 +0200
    13.3 @@ -35,10 +35,10 @@
    13.4  
    13.5  val show_consts = Goal_Display.show_consts;
    13.6  
    13.7 -val show_hyps_raw = Config.declare "show_hyps" (fn _ => Config.Bool false);
    13.8 +val show_hyps_raw = Config.declare ("show_hyps", @{here}) (fn _ => Config.Bool false);
    13.9  val show_hyps = Config.bool show_hyps_raw;
   13.10  
   13.11 -val show_tags_raw = Config.declare "show_tags" (fn _ => Config.Bool false);
   13.12 +val show_tags_raw = Config.declare ("show_tags", @{here}) (fn _ => Config.Bool false);
   13.13  val show_tags = Config.bool show_tags_raw;
   13.14  
   13.15  
    14.1 --- a/src/Pure/goal_display.ML	Sun Apr 06 15:51:02 2014 +0200
    14.2 +++ b/src/Pure/goal_display.ML	Sun Apr 06 16:36:28 2014 +0200
    14.3 @@ -23,13 +23,13 @@
    14.4  structure Goal_Display: GOAL_DISPLAY =
    14.5  struct
    14.6  
    14.7 -val goals_limit_raw = Config.declare_option "goals_limit";
    14.8 +val goals_limit_raw = Config.declare_option ("goals_limit", @{here});
    14.9  val goals_limit = Config.int goals_limit_raw;
   14.10  
   14.11 -val show_main_goal_raw = Config.declare_option "show_main_goal";
   14.12 +val show_main_goal_raw = Config.declare_option ("show_main_goal", @{here});
   14.13  val show_main_goal = Config.bool show_main_goal_raw;
   14.14  
   14.15 -val show_consts_raw = Config.declare_option "show_consts";
   14.16 +val show_consts_raw = Config.declare_option ("show_consts", @{here});
   14.17  val show_consts = Config.bool show_consts_raw;
   14.18  
   14.19  fun pretty_flexpair ctxt (t, u) = Pretty.block
    15.1 --- a/src/Pure/pattern.ML	Sun Apr 06 15:51:02 2014 +0200
    15.2 +++ b/src/Pure/pattern.ML	Sun Apr 06 16:36:28 2014 +0200
    15.3 @@ -42,7 +42,8 @@
    15.4  
    15.5  val unify_trace_failure_default = Unsynchronized.ref false;
    15.6  val unify_trace_failure_raw =
    15.7 -  Config.declare_global "unify_trace_failure" (fn _ => Config.Bool (! unify_trace_failure_default));
    15.8 +  Config.declare_global ("unify_trace_failure", @{here})
    15.9 +    (fn _ => Config.Bool (! unify_trace_failure_default));
   15.10  val unify_trace_failure = Config.bool unify_trace_failure_raw;
   15.11  
   15.12  fun string_of_term thy env binders t =
    16.1 --- a/src/Pure/raw_simplifier.ML	Sun Apr 06 15:51:02 2014 +0200
    16.2 +++ b/src/Pure/raw_simplifier.ML	Sun Apr 06 16:36:28 2014 +0200
    16.3 @@ -394,12 +394,13 @@
    16.4  
    16.5  (* simp depth *)
    16.6  
    16.7 -val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
    16.8 +val simp_depth_limit_raw = Config.declare ("simp_depth_limit", @{here}) (K (Config.Int 100));
    16.9  val simp_depth_limit = Config.int simp_depth_limit_raw;
   16.10  
   16.11  val simp_trace_depth_limit_default = Unsynchronized.ref 1;
   16.12 -val simp_trace_depth_limit_raw = Config.declare "simp_trace_depth_limit"
   16.13 -  (fn _ => Config.Int (! simp_trace_depth_limit_default));
   16.14 +val simp_trace_depth_limit_raw =
   16.15 +  Config.declare ("simp_trace_depth_limit", @{here})
   16.16 +    (fn _ => Config.Int (! simp_trace_depth_limit_default));
   16.17  val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw;
   16.18  
   16.19  fun inc_simp_depth ctxt =
   16.20 @@ -418,11 +419,12 @@
   16.21  
   16.22  exception SIMPLIFIER of string * thm list;
   16.23  
   16.24 -val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
   16.25 +val simp_debug_raw = Config.declare ("simp_debug", @{here}) (K (Config.Bool false));
   16.26  val simp_debug = Config.bool simp_debug_raw;
   16.27  
   16.28  val simp_trace_default = Unsynchronized.ref false;
   16.29 -val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default));
   16.30 +val simp_trace_raw =
   16.31 +  Config.declare ("simp_trace", @{here}) (fn _ => Config.Bool (! simp_trace_default));
   16.32  val simp_trace = Config.bool simp_trace_raw;
   16.33  
   16.34  fun cond_warning ctxt msg =
    17.1 --- a/src/Pure/skip_proof.ML	Sun Apr 06 15:51:02 2014 +0200
    17.2 +++ b/src/Pure/skip_proof.ML	Sun Apr 06 16:36:28 2014 +0200
    17.3 @@ -4,6 +4,9 @@
    17.4  Skip proof via oracle invocation.
    17.5  *)
    17.6  
    17.7 +val quick_and_dirty_raw = Config.declare_option ("quick_and_dirty", @{here});
    17.8 +val quick_and_dirty = Config.bool quick_and_dirty_raw;
    17.9 +
   17.10  signature SKIP_PROOF =
   17.11  sig
   17.12    val report: Proof.context -> unit
    18.1 --- a/src/Pure/type_infer_context.ML	Sun Apr 06 15:51:02 2014 +0200
    18.2 +++ b/src/Pure/type_infer_context.ML	Sun Apr 06 16:36:28 2014 +0200
    18.3 @@ -20,7 +20,8 @@
    18.4  
    18.5  (* constraints *)
    18.6  
    18.7 -val const_sorts = Config.bool (Config.declare "const_sorts" (K (Config.Bool true)));
    18.8 +val const_sorts =
    18.9 +  Config.bool (Config.declare ("const_sorts", @{here}) (K (Config.Bool true)));
   18.10  
   18.11  fun const_type ctxt =
   18.12    try ((not (Config.get ctxt const_sorts) ? Type.strip_sorts) o
    19.1 --- a/src/Pure/unify.ML	Sun Apr 06 15:51:02 2014 +0200
    19.2 +++ b/src/Pure/unify.ML	Sun Apr 06 16:36:28 2014 +0200
    19.3 @@ -34,19 +34,19 @@
    19.4  (*Unification options*)
    19.5  
    19.6  (*tracing starts above this depth, 0 for full*)
    19.7 -val trace_bound_raw = Config.declare_global "unify_trace_bound" (K (Config.Int 50));
    19.8 +val trace_bound_raw = Config.declare_global ("unify_trace_bound", @{here}) (K (Config.Int 50));
    19.9  val trace_bound = Config.int trace_bound_raw;
   19.10  
   19.11  (*unification quits above this depth*)
   19.12 -val search_bound_raw = Config.declare_global "unify_search_bound" (K (Config.Int 60));
   19.13 +val search_bound_raw = Config.declare_global ("unify_search_bound", @{here}) (K (Config.Int 60));
   19.14  val search_bound = Config.int search_bound_raw;
   19.15  
   19.16  (*print dpairs before calling SIMPL*)
   19.17 -val trace_simp_raw = Config.declare_global "unify_trace_simp" (K (Config.Bool false));
   19.18 +val trace_simp_raw = Config.declare_global ("unify_trace_simp", @{here}) (K (Config.Bool false));
   19.19  val trace_simp = Config.bool trace_simp_raw;
   19.20  
   19.21  (*announce potential incompleteness of type unification*)
   19.22 -val trace_types_raw = Config.declare_global "unify_trace_types" (K (Config.Bool false));
   19.23 +val trace_types_raw = Config.declare_global ("unify_trace_types", @{here}) (K (Config.Bool false));
   19.24  val trace_types = Config.bool trace_types_raw;
   19.25  
   19.26