# HG changeset patch
# User blanchet
# Date 1272384166 -7200
# Node ID db71041b596b43b4f396c6e3ba97085b1b025736
# Parent  1281be23bd23d4cb6a52009170144978bb0fa7a9
remove Nitpick functions that are now implemented in Sledgehammer

diff -r 1281be23bd23 -r db71041b596b src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Apr 27 18:01:41 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Apr 27 18:02:46 2010 +0200
@@ -248,20 +248,11 @@
 
 val pstrs = Pretty.breaks o map Pretty.str o space_explode " "
 
-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 is_long_identifier = forall Syntax.is_identifier o space_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
-           OuterKeyword.is_keyword s) ? quote
-  end
+val unyxml = Sledgehammer_Util.unyxml
+val maybe_quote = Sledgehammer_Util.maybe_quote
 
 (* This hash function is recommended in Compilers: Principles, Techniques, and
-   Tools, by Aho, Sethi and Ullman. The hashpjw function, which they
+   Tools, by Aho, Sethi, and Ullman. The "hashpjw" function, which they
    particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *)
 fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w))
 fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w)