src/Tools/nbe.ML
changeset 28227 77221ee0f7b9
parent 28054 2b84d34c5d02
child 28274 9873697fa411
     1.1 --- a/src/Tools/nbe.ML	Mon Sep 15 20:51:58 2008 +0200
     1.2 +++ b/src/Tools/nbe.ML	Tue Sep 16 09:21:22 2008 +0200
     1.3 @@ -454,7 +454,8 @@
     1.4    let val ctxt = Toplevel.context_of state
     1.5    in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
     1.6  
     1.7 -val setup = Theory.add_oracle ("norm", norm_oracle);
     1.8 +val setup = Theory.add_oracle ("norm", norm_oracle)
     1.9 +  #> Value.add_evaluator ("nbe", norm_term o ProofContext.theory_of);
    1.10  
    1.11  local structure P = OuterParse and K = OuterKeyword in
    1.12  
    1.13 @@ -462,7 +463,7 @@
    1.14  
    1.15  val _ =
    1.16    OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag
    1.17 -    (opt_modes -- P.typ >> (Toplevel.keep o norm_print_term_cmd));
    1.18 +    (opt_modes -- P.term >> (Toplevel.keep o norm_print_term_cmd));
    1.19  
    1.20  end;
    1.21