proper separation of static and dynamic context
authorhaftmann
Thu May 15 16:38:31 2014 +0200 (2014-05-15)
changeset 56972f64730f667b9
parent 56971 f4942eb3bb03
child 56973 62da80041afd
proper separation of static and dynamic context
src/Tools/nbe.ML
     1.1 --- a/src/Tools/nbe.ML	Thu May 15 16:38:30 2014 +0200
     1.2 +++ b/src/Tools/nbe.ML	Thu May 15 16:38:31 2014 +0200
     1.3 @@ -600,13 +600,13 @@
     1.4  fun static_conv ctxt consts =
     1.5    let
     1.6      val evaluator = Code_Thingol.static_conv ctxt consts
     1.7 -      (fn program => fn _ => K (oracle ctxt (compile true ctxt program)));
     1.8 +      (fn program => fn _ => fn ctxt' => oracle ctxt' (compile true ctxt program));
     1.9    in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end;
    1.10  
    1.11  fun static_value ctxt consts =
    1.12    let
    1.13      val evaluator = Code_Thingol.static_value ctxt I consts
    1.14 -      (fn program => fn _ => K (eval_term ctxt (compile false ctxt program)));
    1.15 +      (fn program => fn _ => fn ctxt' => eval_term ctxt' (compile false ctxt program));
    1.16    in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
    1.17  
    1.18  end;