src/Pure/Isar/attrib.ML
changeset 18708 4b3dadb4fe33
parent 18678 dd0c569fa43d
child 18734 f5ea6b0d3501
     1.1 --- a/src/Pure/Isar/attrib.ML	Thu Jan 19 15:45:10 2006 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu Jan 19 21:22:08 2006 +0100
     1.3 @@ -114,7 +114,7 @@
     1.4      end;
     1.5  end);
     1.6  
     1.7 -val _ = Context.add_setup [AttributesData.init];
     1.8 +val _ = Context.add_setup AttributesData.init;
     1.9  val print_attributes = AttributesData.print;
    1.10  
    1.11  
    1.12 @@ -487,7 +487,7 @@
    1.13  (* theory setup *)
    1.14  
    1.15  val _ = Context.add_setup
    1.16 - [add_attributes
    1.17 + (add_attributes
    1.18     [("tagged", common tagged, "tagged theorem"),
    1.19      ("untagged", common untagged, "untagged theorem"),
    1.20      ("COMP", common COMP_att, "direct composition with rules (no lifting)"),
    1.21 @@ -511,7 +511,7 @@
    1.22      ("rulify", (no_args ObjectLogic.declare_rulify, no_args undef_local_attribute),
    1.23        "declaration of rulify rule"),
    1.24      ("rule_format", common rule_format_att, "result put into standard rule format"),
    1.25 -    ("attribute", common internal_att, "internal attribute")]];
    1.26 +    ("attribute", common internal_att, "internal attribute")]);
    1.27  
    1.28  end;
    1.29