| changeset 4651 | 70dd492a1698 |
| parent 4556 | e7a4683c0026 |
| child 4686 | 74a12e86b20b |
--- a/src/HOL/Auth/Message.ML Wed Feb 25 15:48:04 1998 +0100 +++ b/src/HOL/Auth/Message.ML Wed Feb 25 15:51:24 1998 +0100 @@ -316,7 +316,7 @@ by (blast_tac (claset() addSEs [add_leE]) 2); (*Nonce case*) by (res_inst_tac [("x","N + Suc nat")] exI 1); -by (fast_tac (claset() addSEs [add_leE] addaltern trans_tac) 1); +by (fast_tac (claset() addSEs [add_leE] addaltern ("trans_tac",trans_tac)) 1); qed "msg_Nonce_supply";