Quot/Examples/LarryDatatype.thy
changeset 766 df053507edba
parent 723 93dce7c71929
child 767 37285ec4387d
--- 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*}