--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Aug 13 18:31:40 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Aug 13 18:53:24 2024 +0200
@@ -149,9 +149,9 @@
fun regularize_tac ctxt =
let
val simpset =
- mk_minimal_simpset ctxt
- addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
- addsimprocs [regularize_simproc]
+ (mk_minimal_simpset ctxt
+ addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
+ |> Simplifier.add_proc regularize_simproc)
addSolver equiv_solver addSolver quotient_solver
val eq_eqvs = eq_imp_rel_get ctxt
in