diff -r 636458836fca -r 1ed073555e6b src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Sun Aug 18 15:08:32 2024 +0200
+++ b/src/HOL/Tools/groebner.ML	Sun Aug 18 15:21:50 2024 +0200
@@ -895,7 +895,7 @@
   | \<^Const_>\<open>disj for _ _\<close> => find_args tm ctxt
   | \<^Const_>\<open>implies for _ _\<close> => find_args tm ctxt
   | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args tm ctxt
-  | Const("(==)",_)$_$_ => find_args tm ctxt  (* FIXME proper const name *)
+  | \<^Const_>\<open>Pure.eq _ for _ _\<close> => find_args tm ctxt
   | \<^Const_>\<open>Trueprop for _\<close> => find_term (Thm.dest_arg tm) ctxt
   | _ => raise TERM ("find_term", []))
 and find_args tm ctxt =