src/Tools/Code/code_preproc.ML

   val cert: code_graph -> string -> Code.cert
   val sortargs: code_graph -> string -> sort list
   val all: code_graph -> string list
   val pretty: theory -> code_graph -> Pretty.T
   val obtain: theory -> string list -> term list -> code_algebra * code_graph
-  val eval_conv: theory
+  val dynamic_eval_conv: theory
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm
-  val eval: theory -> ((term -> term) -> 'a -> 'a)
+  val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
   val pre_post_conv: theory -> (cterm -> thm) -> cterm -> thm
 
   val setup: theory -> theory
 end

 
 fun delete_force msg key xs =
   if AList.defined (op =) xs key then AList.delete (op =) key xs
   else error ("No such " ^ msg ^ ": " ^ quote key);
 
-fun map_data f = Code.purge_data
-  #> (Code_Preproc_Data.map o map_thmproc) f;
+val map_data = Code_Preproc_Data.map o map_thmproc;
 
 val map_pre_post = map_data o apfst;
 val map_pre = map_pre_post o apfst;
 val map_post = map_pre_post o apsnd;
 

 (** retrieval and evaluation interfaces **)
 
 fun obtain thy cs ts = apsnd snd
   (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
 
-fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct =
+fun dynamic_eval thy cterm_of conclude_evaluation evaluator proto_ct =
   let
     val pp = Syntax.pp_global thy;
     val ct = cterm_of proto_ct;
     val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp)
       (Thm.term_of ct);

     val consts = fold_aterms
       (fn Const (c, _) => insert (op =) c | _ => I) t' [];
     val (algebra', eqngr') = obtain thy consts [t'];
   in conclude_evaluation (evaluator algebra' eqngr' vs t' ct') thm end;
 
-fun simple_evaluator evaluator algebra eqngr vs t ct =
-  evaluator algebra eqngr vs t;
-
-fun eval_conv thy =
+fun dynamic_eval_conv thy =
   let
     fun conclude_evaluation thm2 thm1 =
       let
         val thm3 = postprocess_conv thy (Thm.rhs_of thm2);
       in
         Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
           error ("could not construct evaluation proof:\n"
           ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
       end;
-  in gen_eval thy I conclude_evaluation end;
-
-fun eval thy postproc evaluator = gen_eval thy (Thm.cterm_of thy)
-  (K o postproc (postprocess_term thy)) (simple_evaluator evaluator);
+  in dynamic_eval thy I conclude_evaluation end;
+
+fun dynamic_eval_value thy postproc evaluator = dynamic_eval thy (Thm.cterm_of thy)
+  (K o postproc (postprocess_term thy)) (K oooo evaluator);
 
 fun pre_post_conv thy conv = (preprocess_conv thy) then_conv conv then_conv (postprocess_conv thy);
 
 
 (** setup **)