src/Pure/Syntax/syntax.ML

--- a/src/Pure/Syntax/syntax.ML	Mon Sep 20 12:03:11 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Sep 20 15:08:51 2010 +0200
@@ -167,7 +167,7 @@
 fun read_token str =
   let
     val tree = YXML.parse str handle Fail msg => error msg;
-    val text = Buffer.empty |> XML.add_content tree |> Buffer.content;
+    val text = XML.content_of [tree];
     val pos =
       (case tree of
         XML.Elem ((name, props), _) =>