diff -r be361e980acf -r 82c482467d75 ProgTutorial/Advanced.thy
--- a/ProgTutorial/Advanced.thy	Sat Aug 31 08:07:45 2013 +0100
+++ b/ProgTutorial/Advanced.thy	Sun Dec 15 23:49:05 2013 +0000
@@ -546,7 +546,7 @@
   The simplest morphism is the  @{ML_ind identity in Morphism}-morphism defined as
 *}
 
-ML %grayML{*val identity = Morphism.morphism {binding = [], typ = [], term = [], fact = []}*}
+ML %grayML{*val identity = Morphism.morphism "" {binding = [], typ = [], term = [], fact = []}*}
   
 text {*
   Morphisms can be composed with the function @{ML_ind "$>" in Morphism}
@@ -557,7 +557,7 @@
   | trm_phi (t $ s) = (trm_phi t) $ (trm_phi s)
   | trm_phi t = t*}
 
-ML %grayML{*val phi = Morphism.term_morphism trm_phi*}
+ML %grayML{*val phi = Morphism.term_morphism "foo" trm_phi*}
 
 ML %grayML{*Morphism.term phi @{term "P x y"}*}