src/Pure/Isar/attrib.ML
changeset 39128 93a7365fb4ee
parent 39127 e7ecbe86d22e
child 39134 917b4b6ba3d2
equal deleted inserted replaced
39127:e7ecbe86d22e 39128:93a7365fb4ee
   393 
   393 
   394 val _ = Context.>> (Context.map_theory
   394 val _ = Context.>> (Context.map_theory
   395  (register_config Syntax.show_structs_value #>
   395  (register_config Syntax.show_structs_value #>
   396   register_config Syntax.show_question_marks_value #>
   396   register_config Syntax.show_question_marks_value #>
   397   register_config Syntax.ambiguity_level_value #>
   397   register_config Syntax.ambiguity_level_value #>
       
   398   register_config Syntax.eta_contract_value #>
   398   register_config Goal_Display.goals_limit_value #>
   399   register_config Goal_Display.goals_limit_value #>
   399   register_config Goal_Display.show_main_goal_value #>
   400   register_config Goal_Display.show_main_goal_value #>
   400   register_config Goal_Display.show_consts_value #>
   401   register_config Goal_Display.show_consts_value #>
   401   register_config Unify.trace_bound_value #>
   402   register_config Unify.trace_bound_value #>
   402   register_config Unify.search_bound_value #>
   403   register_config Unify.search_bound_value #>