--- a/src/HOL/Auth/Message.thy Thu Dec 22 13:31:58 2005 +0100
+++ b/src/HOL/Auth/Message.thy Thu Dec 22 14:22:11 2005 +0100
@@ -252,8 +252,9 @@
text{*Cut*}
lemma parts_cut:
- "[| Y\<in> parts (insert X G); X\<in> parts H |] ==> Y\<in> parts (G \<union> H)"
-by (erule parts_trans, auto)
+ "[| Y\<in> parts (insert X G); X\<in> parts H |] ==> Y\<in> parts (G \<union> H)"
+by (blast intro: parts_trans)
+
lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H"
by (force dest!: parts_cut intro: parts_insertI)