src/Tools/Code/code_runtime.ML

     val _ = if ! trace
       then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t))
       else ()
     fun evaluator naming program ((_, vs_ty), t) deps =
       base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args;
-  in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end;
+  in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end;
 
 fun dynamic_value_strict cookie thy some_target postproc t args =
   Exn.release (dynamic_value_exn cookie thy some_target postproc t args);
 
 fun dynamic_value cookie thy some_target postproc t args =

 fun static_value_exn cookie thy some_target postproc consts =
   let
     val serializer = obtain_serializer thy some_target;
     fun evaluator naming program thy ((_, vs_ty), t) deps =
       base_evaluator cookie serializer naming thy program (vs_ty, t) deps [];
-  in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end;
+  in Code_Thingol.static_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end;
 
 fun static_value_strict cookie thy some_target postproc consts t =
   Exn.release (static_value_exn cookie thy some_target postproc consts t);
 
 fun static_value cookie thy some_target postproc consts t =

   fn (serializer, naming, thy, program, vs_t, deps, ct) => check_holds serializer naming thy program vs_t deps ct)));
 
 fun check_holds_oracle serializer naming thy program ((_, vs_ty), t) deps ct =
   raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct);
 
-val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy
+val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_conv thy
   (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy)
   o reject_vars thy);
 
 fun static_holds_conv thy consts =
   let
     val serializer = obtain_serializer thy NONE;
   in
-    Code_Thingol.static_eval_conv thy consts
+    Code_Thingol.static_conv thy consts
       (fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program)
     o reject_vars thy
   end;