diff -r 065f472c09ab -r f3794c231898 CookBook/Solutions.thy --- a/CookBook/Solutions.thy Tue Dec 16 17:37:39 2008 +0100 +++ b/CookBook/Solutions.thy Tue Dec 16 17:28:05 2008 +0000 @@ -34,7 +34,7 @@ val end_cmt = Scan.this_string "*)" in begin_cmt |-- Scan.repeat (Scan.unless end_cmt any) --| end_cmt - >> (enclose "(**" "**)" o implode) + >> (enclose "(**" "**)" o implode) end val scan_all = @@ -43,8 +43,9 @@ *} text {* - By using @{ML_text "#> fst"} in the last line, the function - @{ML scan_all} retruns a string instead of a pair. For example: + By using @{text "#> fst"} in the last line, the function + @{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\""}