--- a/src/HOL/Auth/Public.thy Wed Mar 12 22:57:50 2014 +0100
+++ b/src/HOL/Auth/Public.thy Thu Mar 13 07:07:07 2014 +0100
@@ -414,7 +414,7 @@
(*Tactic for possibility theorems*)
fun possibility_tac ctxt =
REPEAT (*omit used_Says so that Nonces start from different traces!*)
- (ALLGOALS (simp_tac (ctxt delsimps [@{thm used_Says}]))
+ (ALLGOALS (simp_tac (ctxt setSolver safe_solver delsimps [@{thm used_Says}]))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, @{thm Nonce_supply}]))