# HG changeset patch
# User wenzelm
# Date 1723987310 -7200
# Node ID 1ed073555e6b68fb29d6d069c3e5812437c472b2
# Parent  636458836fcae8f4cdeb85a2f009ab2fcff44684
proper const (see also 759bffe1d416 and b2800da9eb8a);

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 =