
diff -r cad35ed6effa -r dc452a1a46e5 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Tue Nov 15 12:49:05 2011 +0100
+++ b/src/HOL/Metis_Examples/Message.thy	Tue Nov 15 12:51:14 2011 +0100
@@ -738,7 +738,7 @@
 
 lemma Fake_parts_insert_in_Un:
      "[|Z \<in> parts (insert X H);  X: synth (analz H)|]
-      ==> Z \<in>  synth (analz H) \<union> parts H";
+      ==> Z \<in>  synth (analz H) \<union> parts H"
 by (blast dest: Fake_parts_insert [THEN subsetD, dest])
 
 declare analz_mono [intro] synth_mono [intro]




