src/Tools/nbe.ML

 *)
 
 signature NBE =
 sig
   val norm_conv: cterm -> thm
-  val norm_term: theory -> term -> term
+  val norm: theory -> term -> term
 
   datatype Univ =
       Const of int * Univ list               (*named (uninterpreted) constants*)
     | Free of string * Univ list             (*free (uninterpreted) variables*)
     | DFree of string * int                  (*free (uninterpreted) dictionary parameters*)

     |> term_of_univ thy program idx_tab
   end;
 
 (* evaluation with type reconstruction *)
 
-fun norm thy naming program (((vs0, (vs, ty)), fs), t) deps =
+fun normalize thy naming program (((vs0, (vs, ty)), fs), t) deps =
   let
     fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
       | t => t);
     val resubst_triv_consts = subst_const (Code_Unit.resubst_alias thy);
     val ty' = typ_of_itype program vs0 ty;

     val rhs = Thm.cterm_of thy raw_rhs;
   in Thm.mk_binop eq lhs rhs end;
 
 val (_, raw_norm_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (Binding.name "norm", fn (thy, naming, program, vsp_ty_fs_t, deps, ct) =>
-    mk_equals thy ct (norm thy naming program vsp_ty_fs_t deps))));
+    mk_equals thy ct (normalize thy naming program vsp_ty_fs_t deps))));
 
 fun norm_oracle thy naming program vsp_ty_fs_t deps ct =
   raw_norm_oracle (thy, naming, program, vsp_ty_fs_t, deps, ct);
 
 fun norm_conv ct =
   let
     val thy = Thm.theory_of_cterm ct;
   in Code_Thingol.eval_conv thy (add_triv_classes thy) (norm_oracle thy) ct end;
 
-fun norm_term thy = Code.postprocess_term thy
-  o Code_Thingol.eval_term thy (add_triv_classes thy) (norm thy);
+fun norm thy = Code_Thingol.eval thy (add_triv_classes thy) I (normalize thy);
 
 (* evaluation command *)
 
 fun norm_print_term ctxt modes t =
   let
     val thy = ProofContext.theory_of ctxt;
-    val t' = norm_term thy t;
+    val t' = norm thy t;
     val ty' = Term.type_of t';
     val ctxt' = Variable.auto_fixes t ctxt;
     val p = PrintMode.with_modes modes (fn () =>
       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();

 
 fun norm_print_term_cmd (modes, s) state =
   let val ctxt = Toplevel.context_of state
   in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
 
-val setup =
-  Value.add_evaluator ("nbe", norm_term o ProofContext.theory_of);
+val setup = Value.add_evaluator ("nbe", norm o ProofContext.theory_of);
 
 local structure P = OuterParse and K = OuterKeyword in
 
 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];