src/HOL/Auth/Public.ML

--- a/src/HOL/Auth/Public.ML	Wed Dec 08 13:51:44 1999 +0100
+++ b/src/HOL/Auth/Public.ML	Wed Dec 08 13:52:36 1999 +0100
@@ -149,7 +149,7 @@
 (*Tactic for possibility theorems*)
 fun possibility_tac st = st |>
     REPEAT (*omit used_Says so that Nonces start from different traces!*)
-    (ALLGOALS (simp_tac (simpset() delsimps [used_Says] setSolver safe_solver))
+    (ALLGOALS (simp_tac (simpset() delsimps [used_Says]))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
                    resolve_tac [refl, conjI, Nonce_supply]));