diff -r ae49c5e8868e -r 32323727af96 ProgTutorial/Advanced.thy
--- a/ProgTutorial/Advanced.thy	Sat Oct 29 12:17:06 2011 +0100
+++ b/ProgTutorial/Advanced.thy	Sun Oct 30 17:45:10 2011 +0000
@@ -187,7 +187,7 @@
   The simplest morphism is the  @{ML_ind identity in Morphism}-morphism defined as
 *}
 
-ML{*val identity = Morphism.morphism {binding = I, typ = I, term = I, fact = I}*}
+ML{*val identity = Morphism.morphism {binding = [], typ = [], term = [], fact = []}*}
   
 text {*
   Morphisms can be composed with the function @{ML_ind "$>" in Morphism}