--- a/ProgTutorial/FirstSteps.thy	Wed Apr 07 11:32:00 2010 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sat Apr 24 22:55:50 2010 +0200
@@ -10,7 +10,7 @@
 *}
 (*>*)
 
-chapter {* First Steps *}
+chapter {* First Steps\label{chp:firststeps} *}
 
 text {*
    \begin{flushright}
@@ -142,12 +142,12 @@
   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_ind makestring in PolyML}:
+  for converting values into strings, namely the antiquotation 
+  @{text "@{make_string}"}:
 
-  @{ML_response_eq [display,gray] "writeln (PolyML.makestring 1)" "\"1\"" with "(op =)"} 
+  @{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""} 
 
-  However, @{ML makestring in PolyML} only works if the type of what
+  However, @{text "@{makes_tring}"} 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,
@@ -797,6 +797,11 @@
   \end{readmore}
 
   \footnote{\bf FIXME: find a good exercise for combinators}
+  \begin{exercise}
+  Find out what the combinator @{ML "K I"} does.
+  \end{exercise}
+
+
   \footnote{\bf FIXME: say something about calling conventions} 
 *}