diff -r 5accec94b6df -r 358f325f4db6 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Fri Jun 05 04:17:28 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Tue Jun 23 04:05:01 2009 +0200
@@ -75,17 +75,17 @@
   In the examples above we use the function @{ML Symbol.explode}, instead of the 
   more standard library function @{ML explode}, for obtaining an input list for 
   the parser. The reason is that @{ML Symbol.explode} is aware of character sequences,
-  for example @{text "\\<foo>"}, that have a special meaning in Isabelle. To see
+  for example @{text "\<foo>"}, that have a special meaning in Isabelle. To see
   the difference consider
 
 @{ML_response_fake [display,gray]
 "let 
-  val input = \"\\<foo> bar\"
+  val input = \"\<foo> bar\"
 in
   (explode input, Symbol.explode input)
 end"
 "([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"],
- [\"\\<foo>\", \" \", \"b\", \"a\", \"r\"])"}
+ [\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"}
 
   Slightly more general than the parser @{ML "$$"} is the function 
   @{ML [index] one in Scan}, in that it takes a predicate as argument and