changeset 24867 | e5b55d7be9bb |
parent 24839 | 199c48ec5a09 |
child 24920 | 2a45e400fdad |
--- a/src/Tools/nbe.ML Sat Oct 06 16:41:22 2007 +0200 +++ b/src/Tools/nbe.ML Sat Oct 06 16:50:04 2007 +0200 @@ -410,12 +410,10 @@ val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) []; -val nbeP = +val _ = OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag (opt_modes -- P.typ >> (Toplevel.keep o norm_print_term_cmd)); -val _ = OuterSyntax.add_parsers [nbeP]; - end; end;