
diff -r b5914f3c643c -r 5b9c6010897b CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Wed Dec 17 05:08:33 2008 +0000
+++ b/CookBook/FirstSteps.thy	Sat Jan 03 20:44:54 2009 +0000
@@ -75,7 +75,7 @@
   then there is a convenient, though again ``quick-and-dirty'', method for
   converting values into strings, for example:
 
-  @{ML_response_fake [display] "warning (makestring 1)" "1"} 
+  @{ML_response_fake [display] "warning (makestring 1)" "\"1\""} 
 
   However this only works if the type of what is converted is monomorphic and is not 
   a function.
@@ -157,7 +157,7 @@
   @{ML_response_fake [display] "@{simpset}" "\<dots>"}
 
   (FIXME: what does a simpset look like? It seems to be the same problem
-  like tokens.)
+  as with tokens.)
 
   While antiquotations nowadays have many applications, they were originally introduced to 
   avoid explicit bindings for theorems such as




