diff -r aedfdcae39a9 -r 242e81f4d461 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Fri Oct 29 13:46:37 2010 +0200
+++ b/ProgTutorial/Parsing.thy	Wed Feb 23 23:55:37 2011 +0000
@@ -90,7 +90,7 @@
   In the examples above we use the function @{ML_ind explode in Symbol} from the
   structure @{ML_struct Symbol}, instead of the more standard library function
   @{ML_ind explode in String}, for obtaining an input list for the parser. The reason is
-  that @{ML explode} in @{ML_struct Symbol} is aware of character
+  that @{ML explode in Symbol} is aware of character
   sequences, for example @{text "\<foo>"}, that have a special meaning in
   Isabelle. To see the difference consider
 
@@ -98,7 +98,7 @@
 "let 
   val input = \"\<foo> bar\"
 in
-  (explode input, Symbol.explode input)
+  (String.explode input, Symbol.explode input)
 end"
 "([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"],
  [\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"}