# HG changeset patch
# User wenzelm
# Date 1368726101 -7200
# Node ID d0ba73d11e32a773d168872d91bef845553c270c
# Parent  837211662fb83585955fcb299d93e27f92f3d7b9
tuned signature;

diff -r 837211662fb8 -r d0ba73d11e32 src/Pure/Isar/attrib.ML
--- 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;
 
diff -r 837211662fb8 -r d0ba73d11e32 src/Pure/config.ML
--- 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