diff -r 1412f84c420a -r d74d0b5052a0 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Thu Sep 29 19:37:20 2005 +0200
+++ b/src/HOL/Auth/Message.thy	Fri Sep 30 09:52:46 2005 +0200
@@ -226,7 +226,8 @@
 
 text{*This allows @{text blast} to simplify occurrences of 
   @{term "parts(G\<union>H)"} in the assumption.*}
-declare parts_Un [THEN equalityD1, THEN subsetD, THEN UnE, elim!] 
+lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE] 
+declare in_parts_UnE [elim!]
 
 
 lemma parts_insert_subset: "insert X (parts H) \<subseteq> parts(insert X H)"