more explicit Config.declare vs. Config.declare_global;

--- a/src/Pure/Isar/attrib.ML	Fri Sep 03 15:54:03 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Sep 03 16:09:12 2010 +0200
@@ -374,7 +374,7 @@
 
 fun declare_config make coerce global name default =
   let
-    val config_value = Config.declare global name (make o default);
+    val config_value = Config.declare_generic {global = global} name (make o default);
     val config = coerce config_value;
   in (config, register_config config_value) end;
 

--- a/src/Pure/Syntax/printer.ML	Fri Sep 03 15:54:03 2010 +0200
+++ b/src/Pure/Syntax/printer.ML	Fri Sep 03 16:09:12 2010 +0200
@@ -58,12 +58,12 @@
 
 val show_free_types_default = Unsynchronized.ref true;
 val show_free_types_value =
-  Config.declare false "show_free_types" (fn _ => Config.Bool (! show_free_types_default));
+  Config.declare "show_free_types" (fn _ => Config.Bool (! show_free_types_default));
 val show_free_types = Config.bool show_free_types_value;
 
 val show_question_marks_default = Unsynchronized.ref true;
 val show_question_marks_value =
-  Config.declare false "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
+  Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
 val show_question_marks = Config.bool show_question_marks_value;
 
 fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),

--- a/src/Pure/config.ML	Fri Sep 03 15:54:03 2010 +0200
+++ b/src/Pure/config.ML	Fri Sep 03 16:09:12 2010 +0200
@@ -22,7 +22,9 @@
   val get_generic: Context.generic -> 'a T -> 'a
   val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
   val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
-  val declare: bool -> string -> (Context.generic -> value) -> value T
+  val declare_generic: {global: bool} -> string -> (Context.generic -> value) -> value T
+  val declare_global: string -> (Context.generic -> value) -> value T
+  val declare: string -> (Context.generic -> value) -> value T
   val name_of: 'a T -> string
 end;
 
@@ -98,7 +100,7 @@
   fun merge data = Inttab.merge (K true) data;
 );
 
-fun declare global name default =
+fun declare_generic {global} name default =
   let
     val id = serial ();
 
@@ -120,6 +122,9 @@
       | map_value f context = update_value f context;
   in Config {name = name, get_value = get_value, map_value = map_value} end;
 
+val declare_global = declare_generic {global = true};
+val declare = declare_generic {global = false};
+
 fun name_of (Config {name, ...}) = name;
 
 

--- a/src/Pure/goal_display.ML	Fri Sep 03 15:54:03 2010 +0200
+++ b/src/Pure/goal_display.ML	Fri Sep 03 16:09:12 2010 +0200
@@ -24,8 +24,7 @@
 
 (*true: show consts with types in proof state output*)
 val show_consts_default = Unsynchronized.ref false;
-val show_consts_value =
-  Config.declare false "show_consts" (fn _ => Config.Bool (! show_consts_default));
+val show_consts_value = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
 val show_consts = Config.bool show_consts_value;
 
 fun pretty_flexpair ctxt (t, u) = Pretty.block

--- a/src/Pure/meta_simplifier.ML	Fri Sep 03 15:54:03 2010 +0200
+++ b/src/Pure/meta_simplifier.ML	Fri Sep 03 16:09:12 2010 +0200
@@ -250,7 +250,7 @@
 
 (* simp depth *)
 
-val simp_depth_limit_value = Config.declare false "simp_depth_limit" (K (Config.Int 100));
+val simp_depth_limit_value = Config.declare "simp_depth_limit" (K (Config.Int 100));
 val simp_depth_limit = Config.int simp_depth_limit_value;
 
 val trace_simp_depth_limit = Unsynchronized.ref 1;
@@ -273,12 +273,11 @@
 
 exception SIMPLIFIER of string * thm;
 
-val debug_simp_value = Config.declare false "debug_simp" (K (Config.Bool false));
+val debug_simp_value = Config.declare "debug_simp" (K (Config.Bool false));
 val debug_simp = Config.bool debug_simp_value;
 
 val trace_simp_default = Unsynchronized.ref false;
-val trace_simp_value =
-  Config.declare false "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
+val trace_simp_value = Config.declare "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
 val trace_simp = Config.bool trace_simp_value;
 
 fun if_enabled (Simpset ({context, ...}, _)) flag f =

--- a/src/Pure/unify.ML	Fri Sep 03 15:54:03 2010 +0200
+++ b/src/Pure/unify.ML	Fri Sep 03 16:09:12 2010 +0200
@@ -32,19 +32,19 @@
 (*Unification options*)
 
 (*tracing starts above this depth, 0 for full*)
-val trace_bound_value = Config.declare true "unify_trace_bound" (K (Config.Int 50));
+val trace_bound_value = Config.declare_global "unify_trace_bound" (K (Config.Int 50));
 val trace_bound = Config.int trace_bound_value;
 
 (*unification quits above this depth*)
-val search_bound_value = Config.declare true "unify_search_bound" (K (Config.Int 60));
+val search_bound_value = Config.declare_global "unify_search_bound" (K (Config.Int 60));
 val search_bound = Config.int search_bound_value;
 
 (*print dpairs before calling SIMPL*)
-val trace_simp_value = Config.declare true "unify_trace_simp" (K (Config.Bool false));
+val trace_simp_value = Config.declare_global "unify_trace_simp" (K (Config.Bool false));
 val trace_simp = Config.bool trace_simp_value;
 
 (*announce potential incompleteness of type unification*)
-val trace_types_value = Config.declare true "unify_trace_types" (K (Config.Bool false));
+val trace_types_value = Config.declare_global "unify_trace_types" (K (Config.Bool false));
 val trace_types = Config.bool trace_types_value;