src/Pure/Isar/attrib.ML
changeset 26463 9283b4185fdf
parent 26435 bdce320cd426
child 26685 40aefd1e8f05
     1.1 --- a/src/Pure/Isar/attrib.ML	Fri Mar 28 19:43:54 2008 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Fri Mar 28 20:02:04 2008 +0100
     1.3 @@ -276,7 +276,7 @@
     1.4  
     1.5  (* theory setup *)
     1.6  
     1.7 -val _ = Context.>>
     1.8 +val _ = Context.>> (Context.map_theory
     1.9   (add_attributes
    1.10     [("attribute", internal_att, "internal attribute"),
    1.11      ("tagged", tagged, "tagged theorem"),
    1.12 @@ -301,7 +301,7 @@
    1.13      ("rule_format", rule_format, "result put into standard rule format"),
    1.14      ("rotated", rotated, "rotated theorem premises"),
    1.15      ("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del,
    1.16 -      "declaration of definitional transformations")]);
    1.17 +      "declaration of definitional transformations")]));
    1.18  
    1.19  
    1.20  
    1.21 @@ -379,12 +379,12 @@
    1.22  
    1.23  (* theory setup *)
    1.24  
    1.25 -val _ = Context.>>
    1.26 +val _ = Context.>> (Context.map_theory
    1.27   (register_config Unify.trace_bound_value #>
    1.28    register_config Unify.search_bound_value #>
    1.29    register_config Unify.trace_simp_value #>
    1.30    register_config Unify.trace_types_value #>
    1.31 -  register_config MetaSimplifier.simp_depth_limit_value);
    1.32 +  register_config MetaSimplifier.simp_depth_limit_value));
    1.33  
    1.34  end;
    1.35