--- a/src/HOL/Tools/record.ML Tue Aug 13 19:28:58 2024 +0200
+++ b/src/HOL/Tools/record.ML Tue Aug 13 21:09:51 2024 +0200
@@ -1442,11 +1442,11 @@
else NONE
end));
- val simprocs = if has_rec goal then [split_simproc P] else [];
+ val add_simproc = if has_rec goal then Simplifier.add_proc (split_simproc P) else I;
val thms' = @{thms o_apply K_record_comp} @ thms;
in
EVERY split_frees_tacs THEN
- full_simp_tac (put_simpset (get_simpset thy) ctxt addsimps thms' addsimprocs simprocs) i
+ full_simp_tac (put_simpset (get_simpset thy) ctxt addsimps thms' |> add_simproc) i
end);