--- a/src/HOL/Tools/ATP/atp_util.ML Sat Jan 24 21:37:31 2015 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Sat Jan 24 22:00:24 2015 +0100
@@ -18,7 +18,6 @@
val find_enclosed : string -> string -> string -> string list
val nat_subscript : int -> string
val unquote_tvar : string -> string
- val unyxml : string -> string
val maybe_quote : Keyword.keywords -> string -> string
val string_of_ext_time : bool * Time.time -> string
val string_of_time : Time.time -> string
@@ -133,11 +132,9 @@
val unquote_tvar = perhaps (try (unprefix "'"))
val unquery_var = perhaps (try (unprefix "?"))
-val unyxml = XML.content_of o YXML.parse_body
-
val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode
fun maybe_quote keywords y =
- let val s = unyxml y in
+ let val s = YXML.content_of y in
y |> ((not (is_long_identifier (unquote_tvar s)) andalso
not (is_long_identifier (unquery_var s))) orelse
Keyword.is_literal keywords s) ? quote