changeset 82695 | d93ead9ac6df |
parent 74561 | 8e6c973003c8 |
--- a/src/ZF/Tools/typechk.ML Thu Jun 12 08:03:05 2025 +0200 +++ b/src/ZF/Tools/typechk.ML Thu Jun 12 12:44:47 2025 +0200 @@ -107,7 +107,8 @@ Simplifier.mk_solver "ZF typecheck" (fn ctxt => type_solver_tac ctxt (Simplifier.prems_of ctxt)); -val _ = Theory.setup (map_theory_simpset (fn ctxt => ctxt setSolver type_solver)); +val _ = + Theory.setup (map_theory_simpset (fn ctxt => ctxt |> Simplifier.set_unsafe_solver type_solver)); (* concrete syntax *)