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