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