--- a/src/HOL/Tools/record.ML Sat Oct 21 14:36:47 2023 +0200
+++ b/src/HOL/Tools/record.ML Sat Oct 21 21:19:02 2023 +0200
@@ -1322,8 +1322,9 @@
P t = ~1: completely split
P t > 0: split up to given bound of record extensions.*)
fun split_simproc P =
- Simplifier.make_simproc \<^context> "record_split"
- {lhss = [\<^term>\<open>x::'a::{}\<close>],
+ Simplifier.make_simproc \<^context>
+ {name = "record_split",
+ lhss = [\<^term>\<open>x::'a::{}\<close>],
proc = fn _ => fn ctxt => fn ct =>
(case Thm.term_of ct of
Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
@@ -1348,7 +1349,8 @@
else NONE
end)
else NONE
- | _ => NONE)};
+ | _ => NONE),
+ identifier = []};
fun ex_sel_eq_proc ctxt ct =
let