diff -r 8f0b2daa7eaa -r d93ead9ac6df src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Thu Jun 12 08:03:05 2025 +0200 +++ b/src/HOL/Orderings.thy Thu Jun 12 12:44:47 2025 +0200 @@ -653,8 +653,8 @@ end setup \ - map_theory_simpset (fn ctxt0 => ctxt0 addSolver - mk_solver "partial and linear orders" (fn ctxt => HOL_Order_Tac.tac (Simplifier.prems_of ctxt) ctxt)) + map_theory_simpset (fn ctxt0 => ctxt0 |> Simplifier.add_unsafe_solver + (mk_solver "partial and linear orders" (fn ctxt => HOL_Order_Tac.tac (Simplifier.prems_of ctxt) ctxt))) \ ML \