diff -r e6ec5283cd22 -r 4d701c0388c3 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Sep 06 19:23:54 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Sep 06 21:33:19 2010 +0200
@@ -324,7 +324,7 @@
 
 structure Configs = Theory_Data
 (
-  type T = Config.value Config.T Symtab.table;
+  type T = Config.raw Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
   fun merge data = Symtab.merge (K true) data;
@@ -392,22 +392,22 @@
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory
- (register_config Syntax.show_brackets_value #>
-  register_config Syntax.show_sorts_value #>
-  register_config Syntax.show_types_value #>
-  register_config Syntax.show_structs_value #>
-  register_config Syntax.show_question_marks_value #>
-  register_config Syntax.ambiguity_level_value #>
-  register_config Syntax.eta_contract_value #>
-  register_config Goal_Display.goals_limit_value #>
-  register_config Goal_Display.show_main_goal_value #>
-  register_config Goal_Display.show_consts_value #>
-  register_config Unify.trace_bound_value #>
-  register_config Unify.search_bound_value #>
-  register_config Unify.trace_simp_value #>
-  register_config Unify.trace_types_value #>
-  register_config MetaSimplifier.simp_depth_limit_value #>
-  register_config MetaSimplifier.debug_simp_value #>
-  register_config MetaSimplifier.trace_simp_value));
+ (register_config Syntax.show_brackets_raw #>
+  register_config Syntax.show_sorts_raw #>
+  register_config Syntax.show_types_raw #>
+  register_config Syntax.show_structs_raw #>
+  register_config Syntax.show_question_marks_raw #>
+  register_config Syntax.ambiguity_level_raw #>
+  register_config Syntax.eta_contract_raw #>
+  register_config Goal_Display.goals_limit_raw #>
+  register_config Goal_Display.show_main_goal_raw #>
+  register_config Goal_Display.show_consts_raw #>
+  register_config Unify.trace_bound_raw #>
+  register_config Unify.search_bound_raw #>
+  register_config Unify.trace_simp_raw #>
+  register_config Unify.trace_types_raw #>
+  register_config MetaSimplifier.simp_depth_limit_raw #>
+  register_config MetaSimplifier.debug_simp_raw #>
+  register_config MetaSimplifier.trace_simp_raw));
 
 end;