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*}