--- a/src/HOL/Tools/groebner.ML Sat Oct 21 14:36:47 2023 +0200
+++ b/src/HOL/Tools/groebner.ML Sat Oct 21 21:19:02 2023 +0200
@@ -779,9 +779,11 @@
let val th = poly_eq_conv ct
in if Thm.is_reflexive th then NONE else SOME th end
in
- Simplifier.cert_simproc (Thm.theory_of_thm idl_sub) "poly_eq_simproc"
- {lhss = [Thm.term_of (Thm.lhs_of idl_sub)],
- proc = Morphism.entity (fn _ => fn _ => proc)}
+ Simplifier.cert_simproc (Thm.theory_of_thm idl_sub)
+ {name = "poly_eq_simproc",
+ lhss = [Thm.term_of (Thm.lhs_of idl_sub)],
+ proc = Morphism.entity (fn _ => fn _ => proc),
+ identifier = []}
end;
val poly_eq_ss =