diff -r a810e8f2f2e9 -r 914a214e110e src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Sun Sep 05 19:47:06 2021 +0200
+++ b/src/HOL/Tools/groebner.ML	Sun Sep 05 21:09:31 2021 +0200
@@ -528,8 +528,7 @@
  fun simp_ex_conv ctxt =
    Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
 
-fun frees t = Drule.cterm_add_frees t [];
-fun free_in v t = member op aconvc (frees t) v;
+fun free_in v t = member op aconvc (Drule.cterm_frees_of t) v;
 
 val vsubst = let
  fun vsubst (t,v) tm =
@@ -737,7 +736,7 @@
       val T = Thm.typ_of_cterm x;
       val all = Thm.cterm_of ctxt (Const (\<^const_name>\<open>All\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
     in Thm.apply all (Thm.lambda x p) end
-  val avs = Drule.cterm_add_frees tm []
+  val avs = Drule.cterm_frees_of tm
   val P' = fold mk_forall avs tm
   val th1 = initial_conv ctxt (mk_neg P')
   val (evs,bod) = strip_exists(concl th1) in
@@ -796,7 +795,7 @@
    val mons = striplist(dest_binary ring_add_tm) t
   in member (op aconvc) mons v andalso
     forall (fn m => v aconvc m
-          orelse not(member (op aconvc) (Drule.cterm_add_frees m []) v)) mons
+          orelse not(member (op aconvc) (Drule.cterm_frees_of m) v)) mons
   end
 
   fun isolate_variable vars tm =
@@ -851,7 +850,7 @@
  fun isolate_monomials vars tm =
  let
   val (cmons,vmons) =
-    List.partition (fn m => null (inter (op aconvc) vars (frees m)))
+    List.partition (fn m => null (inter (op aconvc) vars (Drule.cterm_frees_of m)))
                    (striplist ring_dest_add tm)
   val cofactors = map (fn v => find_multipliers v vmons) vars
   val cnc = if null cmons then zero_tm