changeset 82641 | d22294b20573 |
parent 71916 | 435cdc772110 |
child 82643 | f1c14af17591 |
--- a/src/HOL/Tools/simpdata.ML Wed May 21 10:30:06 2025 +0200 +++ b/src/HOL/Tools/simpdata.ML Wed May 21 10:30:07 2025 +0200 @@ -35,7 +35,7 @@ val ex_comm = @{thm ex_comm} val atomize = let val rules = @{thms atomize_all atomize_imp atomize_eq atomize_conj} - in fn ctxt => Raw_Simplifier.rewrite ctxt true rules end + in fn ctxt => Raw_Simplifier.rewrite_wrt ctxt true rules end ); structure Simpdata =