changeset 78072 | 001739cb8d08 |
parent 74525 | c960bfcb91db |
child 78812 | d769a183d51d |
--- a/src/HOL/Tools/groebner.ML Thu May 18 15:34:01 2023 +0200 +++ b/src/HOL/Tools/groebner.ML Thu May 18 17:21:29 2023 +0200 @@ -781,7 +781,7 @@ in Simplifier.cert_simproc (Thm.theory_of_thm idl_sub) "poly_eq_simproc" {lhss = [Thm.term_of (Thm.lhs_of idl_sub)], - proc = fn _ => fn _ => proc} + proc = Morphism.entity (fn _ => fn _ => proc)} end; val poly_eq_ss =