--- a/ProgTutorial/FirstSteps.thy	Thu Aug 20 22:30:20 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Thu Aug 20 23:30:51 2009 +0200
@@ -115,7 +115,7 @@
   code. This can be done in a ``quick-and-dirty'' fashion using the function
   @{ML_ind  "writeln"}. For example
 
-  @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
+  @{ML_response_eq [display,gray] "writeln \"any string\"" "\"any string\"" with "(op =)"}
 
   will print out @{text [quotes] "any string"} inside the response buffer of
   Isabelle.  This function expects a string as argument. If you develop under
@@ -123,7 +123,7 @@
   for converting values into strings, namely the function 
   @{ML_ind  makestring in PolyML}:
 
-  @{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""} 
+  @{ML_response_eq [display,gray] "writeln (PolyML.makestring 1)" "\"1\"" with "(op =)"} 
 
   However, @{ML makestring in PolyML} only works if the type of what
   is converted is monomorphic and not a function.
@@ -134,7 +134,7 @@
   function @{ML_ind  tracing} is more appropriate. This function writes all
   output into a separate tracing buffer. For example:
 
-  @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
+  @{ML_response_eq [display,gray] "tracing \"foo\"" "\"foo\"" with "(op =)"}
 
   It is also possible to redirect the ``channel'' where the string @{text
   "foo"} is printed to a separate file, e.g., to prevent ProofGeneral from
@@ -210,7 +210,7 @@
 
   @{ML_response_fake [display,gray]
   "string_of_term @{context} @{term \"1::nat\"}"
-  "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
+  "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""} 
 
   This produces a string corrsponding to the term @{term [show_types] "1::nat"} with some
   additional information encoded in it. The string can be properly printed by