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}" "\"} (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