src/Pure/Isar/attrib.ML

--- a/src/Pure/Isar/attrib.ML	Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Isar/attrib.ML	Thu Jan 19 21:22:08 2006 +0100
@@ -114,7 +114,7 @@
     end;
 end);
 
-val _ = Context.add_setup [AttributesData.init];
+val _ = Context.add_setup AttributesData.init;
 val print_attributes = AttributesData.print;
 
 
@@ -487,7 +487,7 @@
 (* theory setup *)
 
 val _ = Context.add_setup
- [add_attributes
+ (add_attributes
    [("tagged", common tagged, "tagged theorem"),
     ("untagged", common untagged, "untagged theorem"),
     ("COMP", common COMP_att, "direct composition with rules (no lifting)"),
@@ -511,7 +511,7 @@
     ("rulify", (no_args ObjectLogic.declare_rulify, no_args undef_local_attribute),
       "declaration of rulify rule"),
     ("rule_format", common rule_format_att, "result put into standard rule format"),
-    ("attribute", common internal_att, "internal attribute")]];
+    ("attribute", common internal_att, "internal attribute")]);
 
 end;