--- a/ProgTutorial/Advanced.thy	Sat Oct 29 13:17:12 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}

--- a/ProgTutorial/Essential.thy	Sat Oct 29 13:17:12 2011 +0100
+++ b/ProgTutorial/Essential.thy	Sun Oct 30 17:45:10 2011 +0000
@@ -2225,7 +2225,7 @@
 *}
 
 ML{*structure MyThms = Named_Thms
-  (val name = "attr_thms" 
+  (val name = @{binding "attr_thms"} 
    val description = "Theorems for an Attribute") *}
 
 text {* 

--- a/ProgTutorial/First_Steps.thy	Sat Oct 29 13:17:12 2011 +0100
+++ b/ProgTutorial/First_Steps.thy	Sun Oct 30 17:45:10 2011 +0000
@@ -1245,7 +1245,7 @@
 *}
 
 ML{*structure FooRules = Named_Thms
-  (val name = "foo" 
+  (val name = @{binding "foo"} 
    val description = "Theorems for foo") *}
 
 text {*

Binary file progtutorial.pdf has changed