src/Tools/Code/code_runtime.ML
changeset 61077 06cca32aa519
parent 60956 10d463883dc2
child 62354 fdd6989cc8a0
     1.1 --- a/src/Tools/Code/code_runtime.ML	Tue Sep 01 22:32:58 2015 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Sep 01 23:10:23 2015 +0200
     1.3 @@ -131,7 +131,7 @@
     1.4        else ()
     1.5      fun evaluator program _ vs_ty_t deps =
     1.6        evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) vs_ty_t args;
     1.7 -  in Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t end;
     1.8 +  in Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t end;
     1.9  
    1.10  fun dynamic_value_strict cookie ctxt some_target postproc t args =
    1.11    Exn.release (dynamic_value_exn cookie ctxt some_target postproc t args);
    1.12 @@ -148,7 +148,7 @@
    1.13  fun static_value_exn cookie { ctxt, target, lift_postproc, consts } =
    1.14    let
    1.15      val evaluator = Code_Thingol.static_value { ctxt = ctxt,
    1.16 -      lift_postproc = Exn.map_result o lift_postproc, consts = consts }
    1.17 +      lift_postproc = Exn.map_res o lift_postproc, consts = consts }
    1.18        (static_evaluator cookie ctxt target);
    1.19    in fn ctxt' => evaluator ctxt' o reject_vars ctxt' end;
    1.20  
    1.21 @@ -314,7 +314,7 @@
    1.22      val cs_code = map (Axclass.unoverload_const thy) consts;
    1.23      val cTs = map2 (fn (_, T) => fn c => (c, T)) consts cs_code;
    1.24      val evaluator = Code_Thingol.static_value { ctxt = ctxt,
    1.25 -      lift_postproc = Exn.map_result o lift_postproc, consts = cs_code }
    1.26 +      lift_postproc = Exn.map_res o lift_postproc, consts = cs_code }
    1.27        (compile_evaluator cookie ctxt cs_code cTs T);
    1.28    in fn ctxt' =>
    1.29      evaluator ctxt' o reject_vars ctxt' o Syntax.check_term ctxt' o Type.constraint T