src/Tools/nbe.ML
changeset 41346 6673f6fa94ca
parent 41247 c5cb19ecbd41
child 41472 f6ab14e61604
     1.1 --- a/src/Tools/nbe.ML	Tue Dec 21 08:40:39 2010 +0100
     1.2 +++ b/src/Tools/nbe.ML	Tue Dec 21 09:18:29 2010 +0100
     1.3 @@ -602,13 +602,13 @@
     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 => let val nbe_program = compile true thy program
     1.8 -      in fn thy => oracle thy program nbe_program end)));
     1.9 +    (K (fn program => fn _ => let val nbe_program = compile true thy program
    1.10 +      in oracle thy program nbe_program end)));
    1.11  
    1.12  fun static_value thy consts = lift_triv_classes_rew thy
    1.13    (Code_Thingol.static_value thy I consts
    1.14 -    (K (fn program => let val nbe_program = compile true thy program
    1.15 -      in fn thy => eval_term thy program (compile false thy program) end)));
    1.16 +    (K (fn program => fn _ => let val nbe_program = compile true thy program
    1.17 +      in eval_term thy program (compile false thy program) end)));
    1.18  
    1.19  
    1.20  (** setup **)