proper const (see also 759bffe1d416 and b2800da9eb8a);
authorwenzelm
Sun, 18 Aug 2024 15:21:50 +0200
changeset 80720 1ed073555e6b
parent 80719 636458836fca
child 80721 ac39d932ddfc
proper const (see also 759bffe1d416 and b2800da9eb8a);
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 =