1.1 --- a/src/Tools/nbe.ML	Thu Apr 19 09:31:36 2012 +0200
     1.2 +++ b/src/Tools/nbe.ML	Thu Apr 19 09:45:49 2012 +0200
     1.3 @@ -605,13 +605,11 @@
     1.4  
     1.5  fun static_conv thy consts =
     1.6    lift_triv_classes_conv thy (Code_Thingol.static_conv thy consts
     1.7 -    (K (fn program => fn _ => let val nbe_program = compile true thy program
     1.8 -      in oracle thy program nbe_program end)));
     1.9 +    (K (fn program => fn _ => oracle thy program (compile true thy program))));
    1.10  
    1.11  fun static_value thy consts = lift_triv_classes_rew thy
    1.12    (Code_Thingol.static_value thy I consts
    1.13 -    (K (fn program => fn _ => let val nbe_program = compile true thy program
    1.14 -      in eval_term thy program (compile false thy program) end)));
    1.15 +    (K (fn program => fn _ => eval_term thy program (compile true thy program))));
    1.16  
    1.17  
    1.18  (** setup **)