changeset 80709 | e6f026505c5b |
parent 80704 | 51525e85fcac |
child 80864 | 1b1f77bcee5f |
--- a/src/HOL/Tools/record.ML Wed Aug 14 18:59:49 2024 +0200 +++ b/src/HOL/Tools/record.ML Wed Aug 14 21:23:22 2024 +0200 @@ -1328,6 +1328,7 @@ fun split_simproc P = Simplifier.make_simproc \<^context> {name = "record_split", + kind = Simproc, lhss = [\<^term>\<open>x::'a::{}\<close>], proc = fn _ => fn ctxt => fn ct => let