diff -r b63c72776f03 -r d111f5988e49 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Wed Apr 15 13:11:08 2009 +0000
+++ b/ProgTutorial/FirstSteps.thy	Sat Apr 25 14:28:58 2009 +0200
@@ -102,9 +102,9 @@
   will print out @{text [quotes] "any string"} inside the response buffer
   of Isabelle.  This function expects a string as argument. If you develop under PolyML,
   then there is a convenient, though again ``quick-and-dirty'', method for
-  converting values into strings, namely the function @{ML makestring}:
+  converting values into strings, namely the function @{ML PolyML.makestring}:
 
-  @{ML_response_fake [display,gray] "writeln (makestring 1)" "\"1\""} 
+  @{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""} 
 
   However, @{ML makestring} only works if the type of what is converted is monomorphic 
   and not a function.
@@ -371,7 +371,7 @@
 
 ML %linenosgray{*fun inc_by_three x =
      x |> (fn x => x + 1)
-       |> tap (fn x => tracing (makestring x))
+       |> tap (fn x => tracing (PolyML.makestring x))
        |> (fn x => x + 2)*}
 
 text {*