diff -r 31e427387ab5 -r 29e308b56d23 src/HOL/Auth/Public.thy
--- 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}]))