src/Tools/nbe.ML
changeset 24867 e5b55d7be9bb
parent 24839 199c48ec5a09
child 24920 2a45e400fdad
     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;