diff -r 7017aee615d6 -r 68841fb382e0 doc-src/Codegen/Thy/document/Introduction.tex
--- a/doc-src/Codegen/Thy/document/Introduction.tex	Mon Nov 16 10:03:58 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Introduction.tex	Mon Nov 16 11:03:14 2009 +0100
@@ -160,7 +160,7 @@
 \hspace*{0pt}\\
 \hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
 \hspace*{0pt}\\
-\hspace*{0pt}val empty :~'a queue = AQueue ([],~[])\\
+\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
 \hspace*{0pt}\\
 \hspace*{0pt}fun dequeue (AQueue ([],~[])) = (NONE,~AQueue ([],~[]))\\
 \hspace*{0pt} ~| dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\