src/HOL/Tools/ATP/atp_util.ML

--- a/src/HOL/Tools/ATP/atp_util.ML	Mon Nov 26 21:10:42 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Mon Nov 26 21:46:04 2012 +0100
@@ -126,7 +126,7 @@
 
 val unyxml = XML.content_of o YXML.parse_body
 
-val is_long_identifier = forall Lexicon.is_identifier o Long_Name.explode
+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