corrected Nbe.static_value: ignore cached compilations;
tuned

--- 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 **)