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>