diff -r ae49c5e8868e -r 32323727af96 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Sat Oct 29 12:17:06 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 {*