
diff -r 817ecad4cf72 -r f65b9f14d5de ProgTutorial/Advanced.thy
--- a/ProgTutorial/Advanced.thy	Tue Jun 28 08:44:34 2011 +0100
+++ b/ProgTutorial/Advanced.thy	Tue Jun 28 09:22:00 2011 +0100
@@ -287,7 +287,6 @@
 *}
 
 text {* 
-  @{ML_ind "Binding.str_of"} returns the string with markup;
   @{ML_ind "Binding.name_of"} returns the string without markup
 
   @{ML_ind "Binding.conceal"} 




