1.1 --- a/src/Tools/Code/code_simp.ML	Tue Sep 21 15:46:06 2010 +0200
     1.2 +++ b/src/Tools/Code/code_simp.ML	Tue Sep 21 15:46:06 2010 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  
     1.5  signature CODE_SIMP =
     1.6  sig
     1.7 -  val no_frees_conv: conv -> conv
     1.8    val map_ss: (simpset -> simpset) -> theory -> theory
     1.9    val dynamic_eval_conv: conv
    1.10    val dynamic_eval_tac: theory -> int -> tactic
    1.11 @@ -19,22 +18,6 @@
    1.12  structure Code_Simp : CODE_SIMP =
    1.13  struct
    1.14  
    1.15 -(* avoid free variables during conversion *)
    1.16 -
    1.17 -fun no_frees_conv conv ct =
    1.18 -  let
    1.19 -    val frees = Thm.add_cterm_frees ct [];
    1.20 -    fun apply_beta free thm = Thm.combination thm (Thm.reflexive free)
    1.21 -      |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
    1.22 -      |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
    1.23 -  in
    1.24 -    ct
    1.25 -    |> fold_rev Thm.cabs frees
    1.26 -    |> conv
    1.27 -    |> fold apply_beta frees
    1.28 -  end;
    1.29 -
    1.30 -
    1.31  (* dedicated simpset *)
    1.32  
    1.33  structure Simpset = Theory_Data
    1.34 @@ -68,8 +51,8 @@
    1.35  
    1.36  (* evaluation with dynamic code context *)
    1.37  
    1.38 -val dynamic_eval_conv = Conv.tap_thy (fn thy => no_frees_conv (Code_Thingol.dynamic_eval_conv thy
    1.39 -  (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program)));
    1.40 +val dynamic_eval_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy
    1.41 +  (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
    1.42  
    1.43  fun dynamic_eval_tac thy = CONVERSION dynamic_eval_conv THEN' conclude_tac thy NONE;
    1.44  
    1.45 @@ -83,9 +66,9 @@
    1.46  
    1.47  (* evaluation with static code context *)
    1.48  
    1.49 -fun static_eval_conv thy some_ss consts = no_frees_conv
    1.50 -  (Code_Thingol.static_eval_conv_simple thy consts
    1.51 -    (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program));
    1.52 +fun static_eval_conv thy some_ss consts =
    1.53 +  Code_Thingol.static_eval_conv_simple thy consts
    1.54 +    (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program);
    1.55  
    1.56  fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
    1.57    THEN' conclude_tac thy some_ss;