diff -r 14c3dd5ee2ad -r 7b8c4fe235aa CookBook/Solutions.thy --- a/CookBook/Solutions.thy Wed Jan 14 21:46:04 2009 +0000 +++ b/CookBook/Solutions.thy Wed Jan 14 23:44:14 2009 +0000 @@ -41,9 +41,9 @@ @{ML scan_all} retruns a string, instead of the pair a parser would normally return. For example: - @{ML_response [display] "scan_all (explode \"foo bar\")" "\"foo bar\""} + @{ML_response [display,gray] "scan_all (explode \"foo bar\")" "\"foo bar\""} - @{ML_response [display] "scan_all (explode \"foo (*test*) bar (*test*)\")" + @{ML_response [display,gray] "scan_all (explode \"foo (*test*) bar (*test*)\")" "\"foo (**test**) bar (**test**)\""} *}