--- a/Quot/Examples/LarryDatatype.thy	Fri Dec 11 19:19:24 2009 +0100
+++ b/Quot/Examples/LarryDatatype.thy	Fri Dec 11 19:19:50 2009 +0100
@@ -119,7 +119,6 @@
   shows "freediscrim U = freediscrim V"
 using a by (induct, auto)
 
-
 subsection{*The Initial Algebra: A Quotiented Message Type*}
 
 quotient  msg = freemsg / msgrel