src/Tools/Code/code_simp.ML
changeset 39475 9cc1ba3c5706
parent 38759 37a9092de102
child 39486 e992bcc4440e
equal deleted inserted replaced
39474:1986f18c4940 39475:9cc1ba3c5706
    82 
    82 
    83 
    83 
    84 (* evaluation with freezed code context *)
    84 (* evaluation with freezed code context *)
    85 
    85 
    86 fun static_eval_conv thy some_ss consts = no_frees_conv
    86 fun static_eval_conv thy some_ss consts = no_frees_conv
    87   (Code_Thingol.static_eval_conv_simple thy consts (rewrite_modulo thy some_ss));
    87   (Code_Thingol.static_eval_conv_simple thy consts
       
    88     (fn program => fn thy => rewrite_modulo thy some_ss program));
    88 
    89 
    89 fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
    90 fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
    90   THEN' conclude_tac thy some_ss;
    91   THEN' conclude_tac thy some_ss;
    91 
    92 
    92 end;
    93 end;