changeset 62913 | 13252110a6fe |
parent 61841 | 4d3527b94f2a |
child 63198 | c583ca33076a |
--- a/src/HOL/Tools/groebner.ML Thu Apr 07 22:09:23 2016 +0200 +++ b/src/HOL/Tools/groebner.ML Fri Apr 08 20:15:20 2016 +0200 @@ -787,7 +787,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, identifier = []} + proc = fn _ => fn _ => proc} end; val poly_eq_ss =