src/Pure/Tools/named_thms.ML
changeset 24867 e5b55d7be9bb
parent 24117 94210ad252e3
child 26363 9d95309f8069
--- a/src/Pure/Tools/named_thms.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/Pure/Tools/named_thms.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -36,10 +36,10 @@
 val setup =
   Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)];
 
-val _ = OuterSyntax.add_parsers
- [OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)
+val _ =
+  OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)
     OuterKeyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
-      Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)))];
+      Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)));
 
 end;