--- a/src/HOL/Tools/ATP/atp_util.ML Mon May 20 11:49:56 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Mon May 20 12:35:29 2013 +0200
@@ -15,6 +15,7 @@
val strip_spaces_except_between_idents : string -> string
val elide_string : int -> string -> string
val nat_subscript : int -> string
+ val unquote_tvar : string -> string
val unyxml : string -> string
val maybe_quote : string -> string
val string_of_ext_time : bool * Time.time -> string
@@ -124,13 +125,16 @@
fun nat_subscript n =
n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
+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 y =
let val s = unyxml y in
- y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
- not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
+ y |> ((not (is_long_identifier (unquote_tvar s)) andalso
+ not (is_long_identifier (unquery_var s))) orelse
Keyword.is_keyword s) ? quote
end