src/HOL/Tools/groebner.ML

  fun mk_exists ctxt v th = Drule.arg_cong_rule (ext ctxt (Thm.typ_of_cterm v))
    (Thm.abstract_rule (getname v) v th)
  fun simp_ex_conv ctxt =
    Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)})
 
-fun free_in v t = member op aconvc (Misc_Legacy.cterm_frees t) v;
+fun free_in v t = Cterms.defined (Misc_Legacy.cterm_frees t) v;
 
 val vsubst = let
  fun vsubst (t,v) tm =
    (Thm.rhs_of o Thm.beta_conversion false) (Thm.apply (Thm.lambda v tm) t)
 in fold vsubst end;

     let
       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 = Misc_Legacy.cterm_frees tm
-  val P' = fold mk_forall avs tm
+  val P' = fold mk_forall (Cterms.list_set_rev avs) tm
   val th1 = initial_conv ctxt (mk_neg P')
   val (evs,bod) = strip_exists(concl th1) in
    if is_forall bod then raise CTERM("ring: non-universal formula",[tm])
    else
    let

     val th2 = fold (fn v => fn th => (Thm.forall_intr v th) COMP allI) evs (th2b RS PFalse)
     val th3 =
       Thm.equal_elim
         (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [not_ex RS sym])
           (th2 |> Thm.cprop_of)) th2
-    in specl avs
+    in specl (Cterms.list_set_rev avs)
              ([[[HOLogic.mk_obj_eq th1, th3 RS PFalse'] MRS trans] MRS PFalse] MRS notnotD)
    end
  end
 fun ideal tms tm ord =
  let

   fun is_defined v t =
   let
    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) (Misc_Legacy.cterm_frees m) v)) mons
+          orelse not(Cterms.defined (Misc_Legacy.cterm_frees m) v)) mons
   end
 
   fun isolate_variable vars tm =
   let
    val th = poly_eq_conv tm

   end
 
  fun isolate_monomials vars tm =
  let
   val (cmons,vmons) =
-    List.partition (fn m => null (inter (op aconvc) vars (Misc_Legacy.cterm_frees m)))
+    List.partition (fn m => null (inter (op aconvc) vars (Cterms.list_set_rev (Misc_Legacy.cterm_frees m))))
                    (striplist ring_dest_add tm)
   val cofactors = map (fn v => find_multipliers v vmons) vars
   val cnc = if null cmons then zero_tm
              else Thm.apply ring_neg_tm
                     (list_mk_binop ring_add_tm cmons)