diff -r 4399175e3014 -r 454a0c895735 src/Pure/config.ML
--- a/src/Pure/config.ML	Thu Aug 02 12:06:27 2007 +0200
+++ b/src/Pure/config.ML	Thu Aug 02 12:06:28 2007 +0200
@@ -24,6 +24,7 @@
   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 name_of: 'a T -> string
 end;
 
 structure Config: CONFIG =
@@ -62,11 +63,14 @@
 (* abstract configuration options *)
 
 datatype 'a T = Config of
- {get_value: Context.generic -> 'a,
+ {name: string,
+  get_value: Context.generic -> 'a,
   map_value: ('a -> 'a) -> Context.generic -> Context.generic};
 
-fun coerce make dest (Config {get_value, map_value}) =
-  Config {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)};
+fun coerce make dest (Config {name, get_value, map_value}) = Config
+ {name = name,
+  get_value = dest o get_value,
+  map_value = fn f => map_value (make o f o dest)};
 
 val bool = coerce Bool (fn Bool b => b);
 val int = coerce Int (fn Int i => i);
@@ -110,7 +114,9 @@
             else context'
           end
       | map_value f context = modify_value f context;
-  in Config {get_value = get_value, map_value = map_value} end;
+  in Config {name = name, get_value = get_value, map_value = map_value} end;
+
+fun name_of (Config {name, ...}) = name;
 
 
 (*final declarations of this structure!*)