Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
changeset 82695 d93ead9ac6df
parent 80634 a90ab1ea6458 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Thu Jun 12 12:44:47 2025 +0200
@@ -36,8 +36,8 @@
 val HOL_basic_ss' =
   simpset_of (put_simpset HOL_basic_ss \<^context>
     addsimps @{thms simp_thms prod.inject}
-    setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
-    setSolver (mk_solver "True_solver" (fn ctxt => resolve_tac ctxt @{thms TrueI})))
+    |> Simplifier.set_unsafe_solver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
+    |> Simplifier.set_unsafe_solver (mk_solver "True_solver" (fn ctxt => resolve_tac ctxt @{thms TrueI})))
 
 
 (* auxillary functions *)
isabelle