diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Isar/context_rules.ML	Thu Jan 19 21:22:08 2006 +0100
@@ -123,7 +123,7 @@
     in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
 );
 
-val _ = Context.add_setup [Rules.init];
+val _ = Context.add_setup Rules.init;
 val print_rules = Rules.print;
 
 
@@ -203,7 +203,7 @@
 val dest_query  = rule_add elim_queryK Tactic.make_elim;
 
 val _ = Context.add_setup
-  [snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [Attrib.theory (intro_query NONE)])]];
+  (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [Attrib.theory (intro_query NONE)])]);
 
 
 (* concrete syntax *)
@@ -222,6 +222,6 @@
   ("rule", Attrib.common (Attrib.syntax (Scan.lift Args.del >> K rule_del)),
     "remove declaration of intro/elim/dest rule")];
 
-val _ = Context.add_setup [Attrib.add_attributes rule_atts];
+val _ = Context.add_setup (Attrib.add_attributes rule_atts);
 
 end;