1.1 --- a/src/Tools/nbe.ML Sat Oct 06 16:41:22 2007 +0200
1.2 +++ b/src/Tools/nbe.ML Sat Oct 06 16:50:04 2007 +0200
1.3 @@ -410,12 +410,10 @@
1.4
1.5 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
1.6
1.7 -val nbeP =
1.8 +val _ =
1.9 OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag
1.10 (opt_modes -- P.typ >> (Toplevel.keep o norm_print_term_cmd));
1.11
1.12 -val _ = OuterSyntax.add_parsers [nbeP];
1.13 -
1.14 end;
1.15
1.16 end;