src/HOL/Auth/Message.thy

--- a/src/HOL/Auth/Message.thy	Fri Mar 09 08:45:53 2007 +0100
+++ b/src/HOL/Auth/Message.thy	Fri Mar 09 08:45:55 2007 +0100
@@ -323,7 +323,7 @@
 apply (induct_tac "msg")
 apply (simp_all (no_asm_simp) add: exI parts_insert2)
  txt{*MPair case: blast works out the necessary sum itself!*}
- prefer 2 apply (blast elim!: add_leE)
+ prefer 2 apply auto apply (blast elim!: add_leE)
 txt{*Nonce case*}
 apply (rule_tac x = "N + Suc nat" in exI, auto) 
 done