# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1319996710 0
# Node ID 32323727af96a17ed7275dec3e972014ee7f007d
# Parent  ae49c5e8868eeedc53e7ba6d34ffd6f9d2c4bd9e# Parent  7a84649d88397bd15da5f0706ec5474abe33f84b
updated

diff -r 7a84649d8839 -r 32323727af96 ProgTutorial/Advanced.thy
--- 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}
diff -r 7a84649d8839 -r 32323727af96 ProgTutorial/Essential.thy
--- 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 {* 
diff -r 7a84649d8839 -r 32323727af96 ProgTutorial/First_Steps.thy
--- 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 {*
diff -r 7a84649d8839 -r 32323727af96 progtutorial.pdf
Binary file progtutorial.pdf has changed