
diff -r d0250d01782c -r df053507edba Quot/Examples/LarryDatatype.thy
--- a/Quot/Examples/LarryDatatype.thy	Sun Dec 20 00:15:40 2009 +0100
+++ b/Quot/Examples/LarryDatatype.thy	Sun Dec 20 00:26:53 2009 +0100
@@ -121,7 +121,7 @@
 
 subsection{*The Initial Algebra: A Quotiented Message Type*}
 
-quotient  msg = freemsg / msgrel
+quotient_type msg = freemsg / msgrel
   by (rule equiv_msgrel)
 
 text{*The abstract message constructors*}




