# 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*)