# HG changeset patch
# User paulson
# Date 854373981 -3600
# Node ID 06b6a499f8aede411b0ee88b267a4a00a762dbd0
# Parent  6e8d130463e3c4e698327bfce3b5904cbf07ca6f
deepen_tac is NOT complete when made to apply "spec" as a safe rule\!\!

diff -r 6e8d130463e3 -r 06b6a499f8ae src/HOL/Auth/Message.ML
--- 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*)