1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Apr 27 14:55:10 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Apr 27 16:00:20 2010 +0200
     1.3 @@ -14,6 +14,8 @@
     1.4    val timestamp : unit -> string
     1.5    val parse_bool_option : bool -> string -> string -> bool option
     1.6    val parse_time_option : string -> string -> Time.time option
     1.7 +  val unyxml : string -> string
     1.8 +  val maybe_quote : string -> string
     1.9  end;
    1.10   
    1.11  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    1.12 @@ -72,4 +74,16 @@
    1.13          SOME (Time.fromMilliseconds msecs)
    1.14      end
    1.15  
    1.16 +fun plain_string_from_xml_tree t =
    1.17 +  Buffer.empty |> XML.add_content t |> Buffer.content
    1.18 +val unyxml = plain_string_from_xml_tree o YXML.parse
    1.19 +
    1.20 +val is_long_identifier = forall Syntax.is_identifier o space_explode "."
    1.21 +fun maybe_quote y =
    1.22 +  let val s = unyxml y in
    1.23 +    y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
    1.24 +           not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
    1.25 +           OuterKeyword.is_keyword s) ? quote
    1.26 +  end
    1.27 +
    1.28  end;