src/Pure/Syntax/syntax.ML

 (* read token -- with optional YXML encoding of position *)
 
 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), _) =>
           if name = Markup.tokenN then Position.of_properties props
           else Position.none