# HG changeset patch
# User wenzelm
# Date 1182724596 -7200
# Node ID c48defc2b28cccbabf57a136be373dd2abd8ea31
# Parent  4a6506fade732a61e2b93db369df1105220a7f1a
made type conv pervasive;
Thm.add_cterm_frees;

diff -r 4a6506fade73 -r c48defc2b28c src/HOL/Tools/Groebner_Basis/groebner.ML
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Mon Jun 25 00:36:35 2007 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Mon Jun 25 00:36:36 2007 +0200
@@ -8,9 +8,9 @@
   val ring_and_ideal_conv :
     {idom: thm list, ring: cterm list * thm list, vars: cterm list,
      semiring: Thm.cterm list * thm list} ->
-    (Thm.cterm -> Rat.rat) -> (Rat.rat -> Thm.cterm) ->
-    Conv.conv ->  Conv.conv ->
-    Conv.conv * (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list)
+    (cterm -> Rat.rat) -> (Rat.rat -> cterm) ->
+    conv ->  conv ->
+    conv * (cterm list -> cterm -> (cterm * cterm -> order) -> cterm list)
     val ring_conv : Proof.context -> cterm -> thm
     val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic
 end
@@ -20,16 +20,6 @@
 open Normalizer;
 open Misc;
 
-     (* FIXME :: Already present in Tools/Presburger/qelim.ML but is much more general!! *)
-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;
-
 fun assocd x al d = case AList.lookup (op =) al x of SOME y => y | NONE => d;
 val rat_0 = Rat.zero;
 val rat_1 = Rat.one;
@@ -680,7 +670,7 @@
  let
   fun mk_forall x p =
       mk_comb (Drule.cterm_rule (instantiate' [SOME (ctyp_of_term x)] []) @{cpat "All:: (?'a => bool) => _"}) (Thm.cabs x p)
-  val avs = cterm_frees tm
+  val avs = Thm.add_cterm_frees tm []
   val P' = fold mk_forall avs tm
   val th1 = initial_conv(mk_neg P')
   val (evs,bod) = strip_exists(concl th1) in