src/Pure/Isar/attrib.ML
changeset 39163 4d701c0388c3
parent 39137 ccb53edd59f0
child 39166 19efc2af3e6c
     1.1 --- a/src/Pure/Isar/attrib.ML	Mon Sep 06 19:23:54 2010 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Mon Sep 06 21:33:19 2010 +0200
     1.3 @@ -324,7 +324,7 @@
     1.4  
     1.5  structure Configs = Theory_Data
     1.6  (
     1.7 -  type T = Config.value Config.T Symtab.table;
     1.8 +  type T = Config.raw Symtab.table;
     1.9    val empty = Symtab.empty;
    1.10    val extend = I;
    1.11    fun merge data = Symtab.merge (K true) data;
    1.12 @@ -392,22 +392,22 @@
    1.13  (* theory setup *)
    1.14  
    1.15  val _ = Context.>> (Context.map_theory
    1.16 - (register_config Syntax.show_brackets_value #>
    1.17 -  register_config Syntax.show_sorts_value #>
    1.18 -  register_config Syntax.show_types_value #>
    1.19 -  register_config Syntax.show_structs_value #>
    1.20 -  register_config Syntax.show_question_marks_value #>
    1.21 -  register_config Syntax.ambiguity_level_value #>
    1.22 -  register_config Syntax.eta_contract_value #>
    1.23 -  register_config Goal_Display.goals_limit_value #>
    1.24 -  register_config Goal_Display.show_main_goal_value #>
    1.25 -  register_config Goal_Display.show_consts_value #>
    1.26 -  register_config Unify.trace_bound_value #>
    1.27 -  register_config Unify.search_bound_value #>
    1.28 -  register_config Unify.trace_simp_value #>
    1.29 -  register_config Unify.trace_types_value #>
    1.30 -  register_config MetaSimplifier.simp_depth_limit_value #>
    1.31 -  register_config MetaSimplifier.debug_simp_value #>
    1.32 -  register_config MetaSimplifier.trace_simp_value));
    1.33 + (register_config Syntax.show_brackets_raw #>
    1.34 +  register_config Syntax.show_sorts_raw #>
    1.35 +  register_config Syntax.show_types_raw #>
    1.36 +  register_config Syntax.show_structs_raw #>
    1.37 +  register_config Syntax.show_question_marks_raw #>
    1.38 +  register_config Syntax.ambiguity_level_raw #>
    1.39 +  register_config Syntax.eta_contract_raw #>
    1.40 +  register_config Goal_Display.goals_limit_raw #>
    1.41 +  register_config Goal_Display.show_main_goal_raw #>
    1.42 +  register_config Goal_Display.show_consts_raw #>
    1.43 +  register_config Unify.trace_bound_raw #>
    1.44 +  register_config Unify.search_bound_raw #>
    1.45 +  register_config Unify.trace_simp_raw #>
    1.46 +  register_config Unify.trace_types_raw #>
    1.47 +  register_config MetaSimplifier.simp_depth_limit_raw #>
    1.48 +  register_config MetaSimplifier.debug_simp_raw #>
    1.49 +  register_config MetaSimplifier.trace_simp_raw));
    1.50  
    1.51  end;