diff -r a0af7fe3f558 -r 5accec94b6df ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Thu Jun 04 09:28:29 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Fri Jun 05 04:17:28 2009 +0200
@@ -122,7 +122,7 @@
 
   @{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""} 
 
-  However, @{ML [index] makestring} only works if the type of what is converted is monomorphic 
+  However, @{ML [index] makestring in PolyML} only works if the type of what is converted is monomorphic 
   and not a function.
 
   The function @{ML "writeln"} should only be used for testing purposes, because any