diff -r 386576a416ea -r ccb223a4d49c src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Sep 20 12:03:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Sep 20 15:08:51 2010 +0200
@@ -70,9 +70,7 @@
 fun nat_subscript n =
   n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
 
-fun plain_string_from_xml_tree t =
-  Buffer.empty |> XML.add_content t |> Buffer.content
-val unyxml = plain_string_from_xml_tree o YXML.parse
+val unyxml = XML.content_of o YXML.parse_body
 
 val is_long_identifier = forall Syntax.is_identifier o space_explode "."
 fun maybe_quote y =