# HG changeset patch
# User haftmann
# Date 1400164711 -7200
# Node ID f64730f667b96c78e3475a66d3ec0dcd3f9f8e73
# Parent  f4942eb3bb031ad8e06e3f6e7bd93b020dd5d1bc
proper separation of static and dynamic context

diff -r f4942eb3bb03 -r f64730f667b9 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu May 15 16:38:30 2014 +0200
+++ b/src/Tools/nbe.ML	Thu May 15 16:38:31 2014 +0200
@@ -600,13 +600,13 @@
 fun static_conv ctxt consts =
   let
     val evaluator = Code_Thingol.static_conv ctxt consts
-      (fn program => fn _ => K (oracle ctxt (compile true ctxt program)));
+      (fn program => fn _ => fn ctxt' => oracle ctxt' (compile true ctxt program));
   in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end;
 
 fun static_value ctxt consts =
   let
     val evaluator = Code_Thingol.static_value ctxt I consts
-      (fn program => fn _ => K (eval_term ctxt (compile false ctxt program)));
+      (fn program => fn _ => fn ctxt' => eval_term ctxt' (compile false ctxt program));
   in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
 
 end;