src/Tools/nbe.ML

   in
     fold_rev add_stmts (Code_Symbol.Graph.strong_conn program)
   end;
 
 
-(** evaluation **)
-
-(* term evaluation by compilation *)
+(** normalization **)
+
+(* term normalization by compilation *)
 
 fun compile_term ctxt nbe_program deps (vs : (string * sort) list, t) =
   let 
     val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
   in

           |> of_univ (bounds + 1) (apps t [BVar (bounds, [])])
           |-> (fn t' => pair (Term.Abs ("u", dummyT, t')))
   in of_univ 0 t 0 |> fst end;
 
 
-(* evaluation with type reconstruction *)
-
-fun eval_term (nbe_program, idx_tab) raw_ctxt t_original ((vs, ty) : typscheme, t) deps =
+(* normalize with type reconstruction *)
+
+fun normalize (nbe_program, idx_tab) raw_ctxt t_original ((vs, ty) : typscheme, t) deps =
   let
     val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
     val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
     fun type_infer t' =
       Syntax.check_term

   in Thm.mk_binop eq lhs rhs end;
 
 val (_, raw_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (@{binding normalization_by_evaluation},
     fn (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct) =>
-      mk_equals ctxt ct (eval_term nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps))));
+      mk_equals ctxt ct (normalize nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps))));
 
 fun oracle nbe_program_idx_tab ctxt vs_ty_t deps ct =
   raw_oracle (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct);
 
 fun dynamic_conv ctxt = lift_triv_classes_conv ctxt
-  (Code_Thingol.dynamic_conv ctxt (fn program => oracle (compile false ctxt program) ctxt));
+  (Code_Thingol.dynamic_conv ctxt (fn program =>
+    oracle (compile false ctxt program) ctxt));
 
 fun dynamic_value ctxt = lift_triv_classes_rew ctxt
-  (Code_Thingol.dynamic_value ctxt I (fn program => eval_term (compile false ctxt program) ctxt));
+  (Code_Thingol.dynamic_value ctxt I (fn program =>
+    normalize (compile false ctxt program) ctxt));
 
 fun static_conv (ctxt_consts as { ctxt, ... }) =
   let
-    val evaluator = Code_Thingol.static_conv_thingol ctxt_consts
+    val conv = Code_Thingol.static_conv_thingol ctxt_consts
       (fn { program, ... } => oracle (compile true ctxt program));
-  in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end;
+  in fn ctxt' => lift_triv_classes_conv ctxt' (conv ctxt') end;
 
 fun static_value { ctxt, consts } =
   let
-    val evaluator = Code_Thingol.static_value { ctxt = ctxt, lift_postproc = I, consts = consts }
-      (fn { program, ... } => eval_term (compile false ctxt program));
-  in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
+    val comp = Code_Thingol.static_value { ctxt = ctxt, lift_postproc = I, consts = consts }
+      (fn { program, ... } => normalize (compile false ctxt program));
+  in fn ctxt' => lift_triv_classes_rew ctxt' (comp ctxt') end;
 
 end;