1.1 --- a/src/HOL/Code_Eval.thy	Fri Apr 24 08:24:52 2009 +0200
     1.2 +++ b/src/HOL/Code_Eval.thy	Fri Apr 24 08:24:54 2009 +0200
     1.3 @@ -161,6 +161,7 @@
     1.4  signature EVAL =
     1.5  sig
     1.6    val mk_term: ((string * typ) -> term) -> (typ -> term) -> term -> term
     1.7 +  val mk_term_of: typ -> term -> term
     1.8    val eval_ref: (unit -> term) option ref
     1.9    val eval_term: theory -> term -> term
    1.10  end;
    1.11 @@ -175,7 +176,7 @@
    1.12  fun eval_term thy t =
    1.13    t 
    1.14    |> Eval.mk_term_of (fastype_of t)
    1.15 -  |> (fn t => Code_ML.eval_term NONE ("Eval.eval_ref", eval_ref) thy t []);
    1.16 +  |> (fn t => Code_ML.eval NONE ("Eval.eval_ref", eval_ref) I thy t []);
    1.17  
    1.18  end;
    1.19  *}

     2.1 --- a/src/HOL/HOL.thy	Fri Apr 24 08:24:52 2009 +0200
     2.2 +++ b/src/HOL/HOL.thy	Fri Apr 24 08:24:54 2009 +0200
     2.3 @@ -1889,7 +1889,7 @@
     2.4      val dummy = @{cprop True};
     2.5    in case try HOLogic.dest_Trueprop t
     2.6     of SOME t' => if Code_ML.eval NONE
     2.7 -         ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' [] 
     2.8 +         ("Eval_Method.eval_ref", Eval_Method.eval_ref) (K I) thy t' [] 
     2.9         then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
    2.10         else dummy
    2.11      | NONE => dummy

     3.1 --- a/src/HOL/Library/Eval_Witness.thy	Fri Apr 24 08:24:52 2009 +0200
     3.2 +++ b/src/HOL/Library/Eval_Witness.thy	Fri Apr 24 08:24:54 2009 +0200
     3.3 @@ -68,7 +68,7 @@
     3.4      | dest_exs _ _ = sys_error "dest_exs";
     3.5    val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
     3.6  in
     3.7 -  if Code_ML.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
     3.8 +  if Code_ML.eval NONE ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) (K I) thy t ws
     3.9    then Thm.cterm_of thy goal
    3.10    else @{cprop True} (*dummy*)
    3.11  end

     4.1 --- a/src/HOL/Library/Quickcheck.thy	Fri Apr 24 08:24:52 2009 +0200
     4.2 +++ b/src/HOL/Library/Quickcheck.thy	Fri Apr 24 08:24:54 2009 +0200
     4.3 @@ -74,8 +74,9 @@
     4.4    let
     4.5      val tys = (map snd o fst o strip_abs) t;
     4.6      val t' = mk_generator_expr thy t tys;
     4.7 -    val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref) thy t' [];
     4.8 -  in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end;
     4.9 +    val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref)
    4.10 +      (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
    4.11 +  in f #> Random_Engine.run end;
    4.12  
    4.13  end
    4.14  *}

     5.1 --- a/src/Tools/code/code_ml.ML	Fri Apr 24 08:24:52 2009 +0200
     5.2 +++ b/src/Tools/code/code_ml.ML	Fri Apr 24 08:24:54 2009 +0200
     5.3 @@ -6,10 +6,8 @@
     5.4  
     5.5  signature CODE_ML =
     5.6  sig
     5.7 -  val eval_term: string option -> string * (unit -> term) option ref
     5.8 -    -> theory -> term -> string list -> term
     5.9    val eval: string option -> string * (unit -> 'a) option ref
    5.10 -    -> theory -> term -> string list -> 'a
    5.11 +    -> ((term -> term) -> 'a -> 'a) -> theory -> term -> string list -> 'a
    5.12    val target_Eval: string
    5.13    val setup: theory -> theory
    5.14  end;
    5.15 @@ -957,7 +955,7 @@
    5.16  
    5.17  (* evaluation *)
    5.18  
    5.19 -fun gen_eval eval some_target reff thy t args =
    5.20 +fun eval some_target reff postproc thy t args =
    5.21    let
    5.22      val ctxt = ProofContext.init thy;
    5.23      val _ = if null (Term.add_frees t []) then () else error ("Term "
    5.24 @@ -976,10 +974,7 @@
    5.25          val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
    5.26            ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
    5.27        in ML_Context.evaluate ctxt false reff sml_code end;
    5.28 -  in eval thy I evaluator t end;
    5.29 -
    5.30 -fun eval_term thy = gen_eval Code_Thingol.eval_term thy;
    5.31 -fun eval thy = gen_eval Code_Thingol.eval thy;
    5.32 +  in Code_Thingol.eval thy I postproc evaluator t end;
    5.33  
    5.34  
    5.35  (* instrumentalization by antiquotation *)

     6.1 --- a/src/Tools/code/code_thingol.ML	Fri Apr 24 08:24:52 2009 +0200
     6.2 +++ b/src/Tools/code/code_thingol.ML	Fri Apr 24 08:24:54 2009 +0200
     6.3 @@ -86,10 +86,7 @@
     6.4    val eval_conv: theory -> (sort -> sort)
     6.5      -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> cterm -> thm)
     6.6      -> cterm -> thm
     6.7 -  val eval_term: theory -> (sort -> sort)
     6.8 -    -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> term)
     6.9 -    -> term -> term
    6.10 -  val eval: theory -> (sort -> sort)
    6.11 +  val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a)
    6.12      -> (naming -> program -> (((string * sort) list * typscheme) * (string * itype) list) * iterm -> string list -> 'a)
    6.13      -> term -> 'a
    6.14  end;
    6.15 @@ -780,8 +777,7 @@
    6.16    in evaluator naming program (((vs'', (vs', ty')), fs'), t') deps end;
    6.17  
    6.18  fun eval_conv thy prep_sort = Code_Wellsorted.eval_conv thy prep_sort o base_evaluator thy;
    6.19 -fun eval_term thy prep_sort = Code_Wellsorted.eval_term thy prep_sort o base_evaluator thy;
    6.20 -fun eval thy prep_sort = Code_Wellsorted.eval thy prep_sort o base_evaluator thy;
    6.21 +fun eval thy prep_sort postproc = Code_Wellsorted.eval thy prep_sort postproc o base_evaluator thy;
    6.22  
    6.23  
    6.24  (** diagnostic commands **)

     7.1 --- a/src/Tools/code/code_wellsorted.ML	Fri Apr 24 08:24:52 2009 +0200
     7.2 +++ b/src/Tools/code/code_wellsorted.ML	Fri Apr 24 08:24:54 2009 +0200
     7.3 @@ -16,9 +16,7 @@
     7.4    val obtain: theory -> string list -> term list -> code_algebra * code_graph
     7.5    val eval_conv: theory -> (sort -> sort)
     7.6      -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm
     7.7 -  val eval_term: theory -> (sort -> sort)
     7.8 -    -> (code_algebra -> code_graph -> (string * sort) list -> term -> term) -> term -> term
     7.9 -  val eval: theory -> (sort -> sort)
    7.10 +  val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a)
    7.11      -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
    7.12  end
    7.13  
    7.14 @@ -334,10 +332,7 @@
    7.15        end;
    7.16    in gen_eval thy I conclude_evaluation end;
    7.17  
    7.18 -fun eval_term thy prep_sort evaluator = gen_eval thy (Thm.cterm_of thy)
    7.19 -  (fn t => K (Code.postprocess_term thy t)) prep_sort (simple_evaluator evaluator);
    7.20 -
    7.21 -fun eval thy prep_sort evaluator = gen_eval thy (Thm.cterm_of thy)
    7.22 -  (fn t => K t) prep_sort (simple_evaluator evaluator);
    7.23 +fun eval thy prep_sort postproc evaluator = gen_eval thy (Thm.cterm_of thy)
    7.24 +  (K o postproc (Code.postprocess_term thy)) prep_sort (simple_evaluator evaluator);
    7.25  
    7.26  end; (*struct*)

     8.1 --- a/src/Tools/nbe.ML	Fri Apr 24 08:24:52 2009 +0200
     8.2 +++ b/src/Tools/nbe.ML	Fri Apr 24 08:24:54 2009 +0200
     8.3 @@ -7,7 +7,7 @@
     8.4  signature NBE =
     8.5  sig
     8.6    val norm_conv: cterm -> thm
     8.7 -  val norm_term: theory -> term -> term
     8.8 +  val norm: theory -> term -> term
     8.9  
    8.10    datatype Univ =
    8.11        Const of int * Univ list               (*named (uninterpreted) constants*)
    8.12 @@ -440,7 +440,7 @@
    8.13  
    8.14  (* evaluation with type reconstruction *)
    8.15  
    8.16 -fun norm thy naming program (((vs0, (vs, ty)), fs), t) deps =
    8.17 +fun normalize thy naming program (((vs0, (vs, ty)), fs), t) deps =
    8.18    let
    8.19      fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
    8.20        | t => t);
    8.21 @@ -483,7 +483,7 @@
    8.22  
    8.23  val (_, raw_norm_oracle) = Context.>>> (Context.map_theory_result
    8.24    (Thm.add_oracle (Binding.name "norm", fn (thy, naming, program, vsp_ty_fs_t, deps, ct) =>
    8.25 -    mk_equals thy ct (norm thy naming program vsp_ty_fs_t deps))));
    8.26 +    mk_equals thy ct (normalize thy naming program vsp_ty_fs_t deps))));
    8.27  
    8.28  fun norm_oracle thy naming program vsp_ty_fs_t deps ct =
    8.29    raw_norm_oracle (thy, naming, program, vsp_ty_fs_t, deps, ct);
    8.30 @@ -493,15 +493,14 @@
    8.31      val thy = Thm.theory_of_cterm ct;
    8.32    in Code_Thingol.eval_conv thy (add_triv_classes thy) (norm_oracle thy) ct end;
    8.33  
    8.34 -fun norm_term thy = Code.postprocess_term thy
    8.35 -  o Code_Thingol.eval_term thy (add_triv_classes thy) (norm thy);
    8.36 +fun norm thy = Code_Thingol.eval thy (add_triv_classes thy) I (normalize thy);
    8.37  
    8.38  (* evaluation command *)
    8.39  
    8.40  fun norm_print_term ctxt modes t =
    8.41    let
    8.42      val thy = ProofContext.theory_of ctxt;
    8.43 -    val t' = norm_term thy t;
    8.44 +    val t' = norm thy t;
    8.45      val ty' = Term.type_of t';
    8.46      val ctxt' = Variable.auto_fixes t ctxt;
    8.47      val p = PrintMode.with_modes modes (fn () =>
    8.48 @@ -516,8 +515,7 @@
    8.49    let val ctxt = Toplevel.context_of state
    8.50    in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
    8.51  
    8.52 -val setup =
    8.53 -  Value.add_evaluator ("nbe", norm_term o ProofContext.theory_of);
    8.54 +val setup = Value.add_evaluator ("nbe", norm o ProofContext.theory_of);
    8.55  
    8.56  local structure P = OuterParse and K = OuterKeyword in
    8.57