# HG changeset patch
# User haftmann
# Date 1334821549 -7200
# Node ID 6244475356ba3f92bc126fe3a7b0be676b77f52b
# Parent  1e18bbfb40cba024bb8c58078892502ec4159c72
corrected Nbe.static_value: ignore cached compilations;
tuned

diff -r 1e18bbfb40cb -r 6244475356ba src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu Apr 19 09:31:36 2012 +0200
+++ b/src/Tools/nbe.ML	Thu Apr 19 09:45:49 2012 +0200
@@ -605,13 +605,11 @@
 
 fun static_conv thy consts =
   lift_triv_classes_conv thy (Code_Thingol.static_conv thy consts
-    (K (fn program => fn _ => let val nbe_program = compile true thy program
-      in oracle thy program nbe_program end)));
+    (K (fn program => fn _ => oracle thy program (compile true thy program))));
 
 fun static_value thy consts = lift_triv_classes_rew thy
   (Code_Thingol.static_value thy I consts
-    (K (fn program => fn _ => let val nbe_program = compile true thy program
-      in eval_term thy program (compile false thy program) end)));
+    (K (fn program => fn _ => eval_term thy program (compile true thy program))));
 
 
 (** setup **)