src/ZF/Tools/typechk.ML
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 *)