diff -r fcc0e6e54dca -r 74846cb0fff9 CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Thu Feb 19 14:44:53 2009 +0000
+++ b/CookBook/Parsing.thy	Fri Feb 20 23:19:41 2009 +0000
@@ -561,24 +561,35 @@
 "(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"}
 
   The function @{ML OuterParse.prop} is similar, except that it gives a different
-  error message, when parsing fails. Looking closer at the result string you will
-  have noticed that the parser not just returns the parsed string, but also some 
-  encoded information. You can see this better if you replace 
-  @{ML Position.none} by @{ML "(Position.line 42)"}, say.
+  error message, when parsing fails. As you can see, the parser not just returns 
+  the parsed string, but also some encoded information. You can decode the
+  information with the function @{ML YXML.parse}. For example
+
+  @{ML_response [display,gray]
+  "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""
+  "XML.Elem (\"token\", [], [XML.Text \"foo\"])"}
+
+  You can see better what is going on if you replace 
+  @{ML Position.none} by @{ML "Position.line 42"}, say:
 
 @{ML_response [display,gray]
 "let 
   val input = OuterSyntax.scan (Position.line 42) \"foo\"
 in 
-  OuterParse.term input
+  YXML.parse (fst (OuterParse.term input))
 end"
-"(\"\\^E\\^Ftoken\\^Fline=42\\^Fend_line=42\\^Efoo\\^E\\^F\\^E\", [])"}
+"XML.Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"}
   
   The positional information is stored so that code called later on will be
   able to give more precise error messages. 
 
+  \begin{readmore}
+  The functions to do with input and outout of XML and YXML are defined 
+  in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}.
+  \end{readmore}
 *}
 
+
 section {* Parsing Specifications\label{sec:parsingspecs} *}
 
 text {*
@@ -707,15 +718,7 @@
  
   The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of
   @{ML thm_name in SpecParse}. As can be seen each theorem name can contain some 
-  attributes. If you want to print out all currently known attributes a theorem 
-  can have, you can use the function:
-
-  @{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}" 
-"COMP:  direct composition with rules (no lifting)
-HOL.dest:  declaration of Classical destruction rule
-HOL.elim:  declaration of Classical elimination rule 
-\<dots>"}
-
+  attributes. 
 
   For the inductive definitions described above only the attibutes @{text "[intro]"} and
   @{text "[simp]"} make sense.