diff -r cecd7a941885 -r 6103b0eadbf2 ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Tue May 14 17:10:47 2019 +0200
+++ b/ProgTutorial/First_Steps.thy	Tue May 14 17:45:13 2019 +0200
@@ -5,7 +5,6 @@
 chapter \<open>First Steps\label{chp:firststeps}\<close>
 
 
-
 text \<open>
   \begin{flushright}
   {\em ``The most effective debugging tool is still careful thought,\\ 
@@ -104,7 +103,7 @@
   for converting values into strings, namely the antiquotation 
   \<open>@{make_string}\<close>:
 
-  @{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""} 
+  @{ML_response_fake [display,gray] \<open>writeln (@{make_string} 1)\<close> \<open>"1"\<close>} 
 
   However, \<open>@{make_string}\<close> only works if the type of what
   is converted is monomorphic and not a function.