# HG changeset patch
# User wenzelm
# Date 1182724595 -7200
# Node ID 4a6506fade732a61e2b93db369df1105220a7f1a
# Parent  881b0497295324fb3a432a309318f517a5e51f76
Thm.add_cterm_frees;

diff -r 881b04972953 -r 4a6506fade73 src/HOL/Tools/Qelim/ferrante_rackoff.ML
--- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Mon Jun 25 00:36:34 2007 +0200
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Mon Jun 25 00:36:35 2007 +0200
@@ -204,17 +204,6 @@
    in h (bounds + 1) b' end;
 in h end;
 
-local
-fun cterm_frees ct = 
- let fun h acc t = 
-   case (term_of t) of 
-    _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
-  | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
-  | Free _ => insert (op aconvc) t acc
-  | _ => acc
- in h [] ct end;
-in
-
 fun raw_ferrack_qe_conv ctxt (thy, {isolate_conv, whatis, simpset}) tm = 
  let 
    val ss = simpset
@@ -223,19 +212,18 @@
               @ [not_all,@{thm "all_not_ex"}, ex_disj_distrib], ss))
     val postcv = Simplifier.rewrite ss
     val nnf = K (nnf_conv then_conv postcv)
-    val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (cterm_frees tm) 
+    val qe_conv = Qelim.gen_qelim_conv ctxt pcv postcv pcv cons (Thm.add_cterm_frees tm []) 
                   (isolate_conv ctxt) nnf
                   (fn vs => ferrack_conv (thy,{isolate_conv = isolate_conv ctxt, 
                                                whatis = whatis, simpset = simpset}) vs
                    then_conv postcv)
- in (Simplifier.rewrite ss then_conv qe_conv) tm
- end
+ in (Simplifier.rewrite ss then_conv qe_conv) tm end;
 
 fun ferrackqe_conv ctxt tm = 
  case Ferrante_Rackoff_Data.match ctxt (grab_atom_bop 0 tm) of
   NONE => error "ferrackqe_conv : no corresponding instance in context!"
 | SOME res => raw_ferrack_qe_conv ctxt res tm
-end;
+
 
 fun core_ferrack_tac ctxt res i st =
  let val p = nth (cprems_of st) (i - 1)