# HG changeset patch
# User haftmann
# Date 1285076766 -7200
# Node ID 7af0441a3a477c9abf7e21e0612ac4ec760d3385
# Parent  6dc866b9c548b7230316c6309ea2b73123a81ff3
no_frees_* is subsumed by new framework mechanisms in Code_Preproc

diff -r 6dc866b9c548 -r 7af0441a3a47 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Tue Sep 21 15:46:06 2010 +0200
+++ b/src/Tools/Code/code_simp.ML	Tue Sep 21 15:46:06 2010 +0200
@@ -6,7 +6,6 @@
 
 signature CODE_SIMP =
 sig
-  val no_frees_conv: conv -> conv
   val map_ss: (simpset -> simpset) -> theory -> theory
   val dynamic_eval_conv: conv
   val dynamic_eval_tac: theory -> int -> tactic
@@ -19,22 +18,6 @@
 structure Code_Simp : CODE_SIMP =
 struct
 
-(* avoid free variables during conversion *)
-
-fun no_frees_conv conv ct =
-  let
-    val frees = Thm.add_cterm_frees ct [];
-    fun apply_beta free thm = Thm.combination thm (Thm.reflexive free)
-      |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false)))
-      |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
-  in
-    ct
-    |> fold_rev Thm.cabs frees
-    |> conv
-    |> fold apply_beta frees
-  end;
-
-
 (* dedicated simpset *)
 
 structure Simpset = Theory_Data
@@ -68,8 +51,8 @@
 
 (* evaluation with dynamic code context *)
 
-val dynamic_eval_conv = Conv.tap_thy (fn thy => no_frees_conv (Code_Thingol.dynamic_eval_conv thy
-  (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program)));
+val dynamic_eval_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy
+  (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
 
 fun dynamic_eval_tac thy = CONVERSION dynamic_eval_conv THEN' conclude_tac thy NONE;
 
@@ -83,9 +66,9 @@
 
 (* evaluation with static code context *)
 
-fun static_eval_conv thy some_ss consts = no_frees_conv
-  (Code_Thingol.static_eval_conv_simple thy consts
-    (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program));
+fun static_eval_conv thy some_ss consts =
+  Code_Thingol.static_eval_conv_simple thy consts
+    (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program);
 
 fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
   THEN' conclude_tac thy some_ss;
diff -r 6dc866b9c548 -r 7af0441a3a47 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Tue Sep 21 15:46:06 2010 +0200
+++ b/src/Tools/nbe.ML	Tue Sep 21 15:46:06 2010 +0200
@@ -589,28 +589,18 @@
 fun oracle thy program nbe_program_idx_tab vsp_ty_t deps ct =
   raw_oracle (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct);
 
-fun no_frees_rew rew t =
-  let
-    val frees = map Free (Term.add_frees t []);
-  in
-    t
-    |> fold_rev lambda frees
-    |> rew
-    |> curry (Term.betapplys o swap) frees
-  end;
-
-val dynamic_eval_conv = Conv.tap_thy (fn thy => Code_Simp.no_frees_conv
-  (lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy
-    (K (fn program => oracle thy program (compile false thy program))))));
+val dynamic_eval_conv = Conv.tap_thy (fn thy =>
+  lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy
+    (K (fn program => oracle thy program (compile false thy program)))));
 
 fun dynamic_eval_value thy = lift_triv_classes_rew thy
-  (no_frees_rew (Code_Thingol.dynamic_eval_value thy I
-    (K (fn program => eval_term thy program (compile false thy program)))));
+  (Code_Thingol.dynamic_eval_value thy I
+    (K (fn program => eval_term thy program (compile false thy program))));
 
-fun static_eval_conv thy consts = Code_Simp.no_frees_conv
-  (lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
+fun static_eval_conv thy consts =
+  lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
     (K (fn program => let val nbe_program = compile true thy program
-      in fn thy => oracle thy program nbe_program end))));
+      in fn thy => oracle thy program nbe_program end)));
 
 
 (** setup **)