# HG changeset patch
# User paulson
# Date 1135257731 -3600
# Node ID b0fe60800623d87f721d696e7aa3fda8f117dd6a
# Parent  1ce410ff9941e982b5104a5d1a93776d0cb55447
shorter proof

diff -r 1ce410ff9941 -r b0fe60800623 src/HOL/Auth/Message.thy
--- 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)