tuned signature;

--- a/src/Pure/Isar/attrib.ML	Thu May 16 17:39:38 2013 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu May 16 19:41:41 2013 +0200
@@ -476,7 +476,7 @@
 fun declare make coerce binding default =
   let
     val name = Binding.name_of binding;
-    val config_value = Config.declare_generic {global = false} name (make o default);
+    val config_value = Config.declare name (make o default);
     val config = coerce config_value;
   in (config, register binding config_value) end;
 

--- a/src/Pure/config.ML	Thu May 16 17:39:38 2013 +0200
+++ b/src/Pure/config.ML	Thu May 16 19:41:41 2013 +0200
@@ -24,7 +24,6 @@
   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_generic: {global: bool} -> string -> (Context.generic -> value) -> raw
   val declare_global: string -> (Context.generic -> value) -> raw
   val declare: string -> (Context.generic -> value) -> raw
   val declare_option: string -> raw
@@ -110,7 +109,7 @@
   fun merge data = Inttab.merge (K true) data;
 );
 
-fun declare_generic {global} name default =
+fun declare_generic global name default =
   let
     val id = serial ();
 
@@ -136,8 +135,8 @@
       | 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};
+val declare_global = declare_generic true;
+val declare = declare_generic false;
 
 fun declare_option name =
   let