src/HOL/Tools/groebner.ML

  fun lhs t = case term_of t of
   Const(@{const_name HOL.eq},_)$_$_ => Thm.dest_arg1 t
  | _=> raise CTERM ("ideal_tac - lhs",[t])
  fun exitac NONE = no_tac
    | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
+
+ val claset = claset_of @{context}
 in
 fun ideal_tac add_ths del_ths ctxt =
   presimplify ctxt add_ths del_ths
  THEN'
  CSUBGOAL (fn (p, i) =>

      val ws = map (exitac o AList.lookup op aconvc cfs) evs
     in EVERY (rev ws) THEN Method.insert_tac prems 1
         THEN ring_tac add_ths del_ths ctxt 1
    end
   in
-     clarify_tac @{context} i
+     clarify_tac (put_claset claset ctxt) i
      THEN Object_Logic.full_atomize_tac i
      THEN asm_full_simp_tac (put_simpset (#poly_eq_ss thy) ctxt) i
-     THEN clarify_tac @{context} i
+     THEN clarify_tac (put_claset claset ctxt) i
      THEN (REPEAT (CONVERSION (#unwind_conv thy ctxt) i))
      THEN SUBPROOF poly_exists_tac ctxt i
   end
  handle TERM _ => no_tac
      | CTERM _ => no_tac