On page 9 (section 5) when defining the translation, you can't break lines the way they are. In particular ... datatype t = ... Ci of taui ... Also, the | should be on both sides of Ci of taui