# HG changeset patch
# User huffman
# Date 1321357874 -3600
# Node ID dc452a1a46e55e133e6f7389ddd8420d80c5005f
# Parent  cad35ed6effae20588bb8d99d720947faea4e837
remove one more old-style semicolon

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]