1.1 --- a/src/Tools/Code/code_runtime.ML	Tue Dec 14 00:16:30 2010 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Wed Dec 15 09:47:12 2010 +0100
     1.3 @@ -120,7 +120,7 @@
     1.4        else ()
     1.5      fun evaluator naming program ((_, vs_ty), t) deps =
     1.6        base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args;
     1.7 -  in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end;
     1.8 +  in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end;
     1.9  
    1.10  fun dynamic_value_strict cookie thy some_target postproc t args =
    1.11    Exn.release (dynamic_value_exn cookie thy some_target postproc t args);
    1.12 @@ -133,7 +133,7 @@
    1.13      val serializer = obtain_serializer thy some_target;
    1.14      fun evaluator naming program thy ((_, vs_ty), t) deps =
    1.15        base_evaluator cookie serializer naming thy program (vs_ty, t) deps [];
    1.16 -  in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end;
    1.17 +  in Code_Thingol.static_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end;
    1.18  
    1.19  fun static_value_strict cookie thy some_target postproc consts t =
    1.20    Exn.release (static_value_exn cookie thy some_target postproc consts t);
    1.21 @@ -175,7 +175,7 @@
    1.22  fun check_holds_oracle serializer naming thy program ((_, vs_ty), t) deps ct =
    1.23    raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct);
    1.24  
    1.25 -val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy
    1.26 +val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_conv thy
    1.27    (fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy)
    1.28    o reject_vars thy);
    1.29  
    1.30 @@ -183,7 +183,7 @@
    1.31    let
    1.32      val serializer = obtain_serializer thy NONE;
    1.33    in
    1.34 -    Code_Thingol.static_eval_conv thy consts
    1.35 +    Code_Thingol.static_conv thy consts
    1.36        (fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program)
    1.37      o reject_vars thy
    1.38    end;