src/Tools/nbe.ML
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;