src/HOL/Auth/Smartcard/Smartcard.thy

     such as  Nonce ?N \<notin> used evs that match Nonce_supply*)
 fun possibility_tac ctxt =
    (REPEAT 
     (ALLGOALS (simp_tac (ctxt
       delsimps @{thms used_Cons_simps}
-      setSolver safe_solver))
+      |> Simplifier.set_unsafe_solver safe_solver))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
                    resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}])))
 
 (*For harder protocols (such as Recur) where we have to set up some
   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]))
 
 val analz_image_freshK_ss = 
   simpset_of