Moved ex_strip_tac to the common part

--- a/src/HOL/Auth/NS_Shared.ML	Thu Oct 24 10:30:43 1996 +0200
+++ b/src/HOL/Auth/NS_Shared.ML	Thu Oct 24 10:31:17 1996 +0200
@@ -387,8 +387,6 @@
 (** The session key K uniquely identifies the message, if encrypted
     with a secure key **)
 
-fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
-
 goal thy 
  "!!evs. evs : ns_shared lost ==>                                            \
 \      EX A' NA' B' X'. ALL A NA B X.                                        \