deepen_tac is NOT complete when made to apply "spec" as a safe rule\!\!

--- a/src/HOL/Auth/Message.ML	Mon Jan 27 15:04:05 1997 +0100
+++ b/src/HOL/Auth/Message.ML	Mon Jan 27 15:06:21 1997 +0100
@@ -868,7 +868,7 @@
           REPEAT o (mp_tac ORELSE' eresolve_tac [asm_rl,exE]),
           (*Duplicate the assumption*)
           forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl,
-          fast_tac (!claset addSDs [spec])];
+          depth_tac (!claset addSDs [spec]) 0];
 
 
 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)