src/Pure/config.ML

   val map_thy: 'a T -> ('a -> 'a) -> theory -> theory
   val put_thy: 'a T -> 'a -> theory -> theory
   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 -> value -> value T
+  val declare: bool -> string -> (Proof.context -> value) -> value T
   val name_of: 'a T -> string
 end;
 
 structure Config: CONFIG =
 struct

 
 fun declare global name default =
   let
     val id = serial ();
 
-    fun get_value context = the_default default (Inttab.lookup (Value.get context) id);
-    fun modify_value f = Value.map (Inttab.map_default (id, default) (type_check name f));
+    fun get_value context =
+      (case Inttab.lookup (Value.get context) id of
+        SOME value => value
+      | NONE => default (Context.proof_of context));
+
+    fun update_value f context =
+      Value.map (Inttab.update (id, type_check name f (get_value context))) context;
 
     fun map_value f (context as Context.Proof _) =
-          let val context' = modify_value f context in
+          let val context' = update_value f context in
             if global andalso
               get_value (Context.Theory (Context.theory_of context')) <> get_value context'
             then (warning ("Ignoring local change of global option " ^ quote name); context)
             else context'
           end
-      | map_value f context = modify_value f context;
+      | map_value f context = update_value f context;
   in Config {name = name, get_value = get_value, map_value = map_value} end;
 
 fun name_of (Config {name, ...}) = name;