src/Tools/code/code_thingol.ML

   val consts_program: theory -> string list -> string list * (naming * program)
   val cached_program: theory -> naming * program
   val eval_conv: theory -> (sort -> sort)
     -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> cterm -> thm)
     -> cterm -> thm
-  val eval_term: theory -> (sort -> sort)
-    -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> term)
-    -> term -> term
-  val eval: theory -> (sort -> sort)
+  val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a)
     -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> 'a)
     -> term -> 'a
 end;
 
 structure Code_Thingol: CODE_THINGOL =

       invoke_generation thy (algebra, funcgr) ensure_value (fs, t);
     val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
   in evaluator naming program (((vs'', (vs', ty')), fs'), t') deps end;
 
 fun eval_conv thy prep_sort = Code_Wellsorted.eval_conv thy prep_sort o base_evaluator thy;
-fun eval_term thy prep_sort = Code_Wellsorted.eval_term thy prep_sort o base_evaluator thy;
-fun eval thy prep_sort = Code_Wellsorted.eval thy prep_sort o base_evaluator thy;
+fun eval thy prep_sort postproc = Code_Wellsorted.eval thy prep_sort postproc o base_evaluator thy;
 
 
 (** diagnostic commands **)
 
 fun code_depgr thy consts =