
diff -r 8f0b2daa7eaa -r d93ead9ac6df src/HOL/SET_Protocol/Public_SET.thy
--- 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>




