src/HOL/SET_Protocol/Public_SET.thy
changeset 82695 d93ead9ac6df
parent 69597 ff784d5a5bfb
--- a/src/HOL/SET_Protocol/Public_SET.thy	Thu Jun 12 08:03:05 2025 +0200
+++ b/src/HOL/SET_Protocol/Public_SET.thy	Thu Jun 12 12:44:47 2025 +0200
@@ -353,7 +353,7 @@
   nonces and keys initially*)
 fun basic_possibility_tac ctxt =
     REPEAT 
-    (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
+    (ALLGOALS (asm_simp_tac (ctxt |> Simplifier.set_unsafe_solver safe_solver))
      THEN
      REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))
 \<close>