src/Pure/Isar/attrib.ML

--- a/src/Pure/Isar/attrib.ML	Sat May 14 17:55:08 2011 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat May 14 18:29:06 2011 +0200
@@ -44,14 +44,6 @@
     (Context.generic -> real) -> real Config.T * (theory -> theory)
   val config_string: Binding.binding ->
     (Context.generic -> string) -> string Config.T * (theory -> theory)
-  val config_bool_global: Binding.binding ->
-    (Context.generic -> bool) -> bool Config.T * (theory -> theory)
-  val config_int_global: Binding.binding ->
-    (Context.generic -> int) -> int Config.T * (theory -> theory)
-  val config_real_global: Binding.binding ->
-    (Context.generic -> real) -> real Config.T * (theory -> theory)
-  val config_string_global: Binding.binding ->
-    (Context.generic -> string) -> string Config.T * (theory -> theory)
   val setup_config_bool: Binding.binding -> (Context.generic -> bool) -> bool Config.T
   val setup_config_int: Binding.binding -> (Context.generic -> int) -> int Config.T
   val setup_config_string: Binding.binding -> (Context.generic -> string) -> string Config.T
@@ -384,24 +376,19 @@
     |> Configs.map (Symtab.update (name, config))
   end;
 
-fun declare make coerce global binding default =
+fun declare make coerce binding default =
   let
     val name = Binding.name_of binding;
-    val config_value = Config.declare_generic {global = global} name (make o default);
+    val config_value = Config.declare_generic {global = false} name (make o default);
     val config = coerce config_value;
   in (config, register binding config_value) end;
 
 in
 
-val config_bool = declare Config.Bool Config.bool false;
-val config_int = declare Config.Int Config.int false;
-val config_real = declare Config.Real Config.real false;
-val config_string = declare Config.String Config.string false;
-
-val config_bool_global = declare Config.Bool Config.bool true;
-val config_int_global = declare Config.Int Config.int true;
-val config_real_global = declare Config.Real Config.real true;
-val config_string_global = declare Config.String Config.string true;
+val config_bool = declare Config.Bool Config.bool;
+val config_int = declare Config.Int Config.int;
+val config_real = declare Config.Real Config.real;
+val config_string = declare Config.String Config.string;
 
 fun register_config config = register (Binding.name (Config.name_of config)) config;