diff -r f3794c231898 -r b5914f3c643c CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Tue Dec 16 17:28:05 2008 +0000
+++ b/CookBook/Parsing.thy	Wed Dec 17 05:08:33 2008 +0000
@@ -304,7 +304,19 @@
 end"
 "((\"hh\", \"ee\"), [\"l\", \"l\", \"o\"])"}
 
-  doubles the two parsed input strings.
+  doubles the two parsed input strings. Or
+
+  @{ML_response [display] 
+"let 
+   val p = Scan.repeat (Scan.one Symbol.not_eof) >> implode
+   val input = (explode \"foo bar foo\") 
+in
+   Scan.finite Symbol.stopper p input
+end" 
+"(\"foo bar foo\",[])"}
+
+  where the single strings in the parsed output are transformed
+  back into one string.
  
   \begin{exercise}\label{ex:scancmts}
   Write a parser that parses an input string so that any comment enclosed