src/Tools/nbe.ML
changeset 39606 7af0441a3a47
parent 39475 9cc1ba3c5706
child 39911 2b4430847310
     1.1 --- a/src/Tools/nbe.ML	Tue Sep 21 15:46:06 2010 +0200
     1.2 +++ b/src/Tools/nbe.ML	Tue Sep 21 15:46:06 2010 +0200
     1.3 @@ -589,28 +589,18 @@
     1.4  fun oracle thy program nbe_program_idx_tab vsp_ty_t deps ct =
     1.5    raw_oracle (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct);
     1.6  
     1.7 -fun no_frees_rew rew t =
     1.8 -  let
     1.9 -    val frees = map Free (Term.add_frees t []);
    1.10 -  in
    1.11 -    t
    1.12 -    |> fold_rev lambda frees
    1.13 -    |> rew
    1.14 -    |> curry (Term.betapplys o swap) frees
    1.15 -  end;
    1.16 -
    1.17 -val dynamic_eval_conv = Conv.tap_thy (fn thy => Code_Simp.no_frees_conv
    1.18 -  (lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy
    1.19 -    (K (fn program => oracle thy program (compile false thy program))))));
    1.20 +val dynamic_eval_conv = Conv.tap_thy (fn thy =>
    1.21 +  lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy
    1.22 +    (K (fn program => oracle thy program (compile false thy program)))));
    1.23  
    1.24  fun dynamic_eval_value thy = lift_triv_classes_rew thy
    1.25 -  (no_frees_rew (Code_Thingol.dynamic_eval_value thy I
    1.26 -    (K (fn program => eval_term thy program (compile false thy program)))));
    1.27 +  (Code_Thingol.dynamic_eval_value thy I
    1.28 +    (K (fn program => eval_term thy program (compile false thy program))));
    1.29  
    1.30 -fun static_eval_conv thy consts = Code_Simp.no_frees_conv
    1.31 -  (lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
    1.32 +fun static_eval_conv thy consts =
    1.33 +  lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
    1.34      (K (fn program => let val nbe_program = compile true thy program
    1.35 -      in fn thy => oracle thy program nbe_program end))));
    1.36 +      in fn thy => oracle thy program nbe_program end)));
    1.37  
    1.38  
    1.39  (** setup **)