diff -r 64fa844064fa -r cc9359bfacf4 CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Wed Mar 04 14:26:21 2009 +0000
+++ b/CookBook/Parsing.thy	Thu Mar 05 16:46:43 2009 +0000
@@ -406,7 +406,7 @@
 *}
 
 ML{*fun filtered_input str = 
-       filter OuterLex.is_proper (OuterSyntax.scan Position.none str) *}
+  filter OuterLex.is_proper (OuterSyntax.scan Position.none str) *}
 
 text {*
 
@@ -594,9 +594,9 @@
   The functions to do with input and output 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 {*