# HG changeset patch
# User wenzelm
# Date 1422133224 -3600
# Node ID 9da5b2c61049cc199ddfa884adab4f447fee57b7
# Parent  42b7b76b37b822e12b6afbca7e9ec9c7accd3d73
tuned signature;

diff -r 42b7b76b37b8 -r 9da5b2c61049 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Jan 24 21:37:31 2015 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Jan 24 22:00:24 2015 +0100
@@ -409,9 +409,6 @@
     create_entry thy thm exec mutants mtds
   end
 
-(* string -> string *)
-val unyxml = XML.content_of o YXML.parse_body
-
 fun string_of_mutant_subentry' thy thm_name (t, results) =
   let
    (* fun string_of_report (Quickcheck.Report {iterations = i, raised_match_errors = e,
@@ -426,8 +423,9 @@
       ^ "(" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"
       (*^ "\n" ^ string_of_reports reports*)
   in
-    "mutant of " ^ thm_name ^ ":\n"
-    ^ unyxml (Syntax.string_of_term_global thy t) ^ "\n" ^ space_implode "; " (map string_of_mtd_result results)
+    "mutant of " ^ thm_name ^ ":\n" ^
+      YXML.content_of (Syntax.string_of_term_global thy t) ^ "\n" ^
+      space_implode "; " (map string_of_mtd_result results)
   end
 
 fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) = 
diff -r 42b7b76b37b8 -r 9da5b2c61049 src/HOL/Tools/ATP/atp_util.ML
--- 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
diff -r 42b7b76b37b8 -r 9da5b2c61049 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 24 21:37:31 2015 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 24 22:00:24 2015 +0100
@@ -320,7 +320,7 @@
 fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
 
 fun quot_normal_name_for_type ctxt T =
-  quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T)
+  quot_normal_prefix ^ YXML.content_of (Syntax.string_of_typ ctxt T)
 
 val strip_first_name_sep =
   Substring.full #> Substring.position name_sep ##> Substring.triml 1
diff -r 42b7b76b37b8 -r 9da5b2c61049 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sat Jan 24 21:37:31 2015 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sat Jan 24 22:00:24 2015 +0100
@@ -303,7 +303,7 @@
 
 fun bound_comment ctxt debug nick T R =
   short_name nick ^
-  (if debug then " :: " ^ unyxml (Syntax.string_of_typ ctxt T) else "") ^
+  (if debug then " :: " ^ YXML.content_of (Syntax.string_of_typ ctxt T) else "") ^
   " : " ^ string_for_rep R
 
 fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) =
diff -r 42b7b76b37b8 -r 9da5b2c61049 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Jan 24 21:37:31 2015 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Jan 24 22:00:24 2015 +0100
@@ -70,7 +70,6 @@
   val eta_expand : typ list -> term -> int -> term
   val DETERM_TIMEOUT : Time.time -> tactic -> tactic
   val indent_size : int
-  val unyxml : string -> string
   val pretty_maybe_quote : Keyword.keywords -> Pretty.T -> Pretty.T
   val hash_term : term -> int
   val spying : bool -> (unit -> Proof.state * int * string) -> unit
@@ -280,8 +279,6 @@
 
 val indent_size = 2
 
-val unyxml = ATP_Util.unyxml
-
 val maybe_quote = ATP_Util.maybe_quote
 
 fun pretty_maybe_quote keywords pretty =
diff -r 42b7b76b37b8 -r 9da5b2c61049 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Jan 24 21:37:31 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Jan 24 22:00:24 2015 +0100
@@ -164,7 +164,7 @@
 
     fun nth_name j =
       (case xref of
-        Facts.Fact s => backquote (simplify_spaces (unyxml s)) ^ bracket
+        Facts.Fact s => backquote (simplify_spaces (YXML.content_of s)) ^ bracket
       | Facts.Named (("", _), _) => "[" ^ bracket ^ "]"
       | Facts.Named ((name, _), NONE) => make_name keywords (length ths > 1) (j + 1) name ^ bracket
       | Facts.Named ((name, _), SOME intervals) =>
diff -r 42b7b76b37b8 -r 9da5b2c61049 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Jan 24 21:37:31 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sat Jan 24 22:00:24 2015 +0100
@@ -140,7 +140,7 @@
   Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x
 
 fun hackish_string_of_term ctxt =
-  with_vanilla_print_mode (Syntax.string_of_term ctxt) #> unyxml #> simplify_spaces
+  with_vanilla_print_mode (Syntax.string_of_term ctxt) #> YXML.content_of #> simplify_spaces
 
 val spying_version = "d"
 
diff -r 42b7b76b37b8 -r 9da5b2c61049 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sat Jan 24 21:37:31 2015 +0100
+++ b/src/Pure/PIDE/yxml.ML	Sat Jan 24 22:00:24 2015 +0100
@@ -26,6 +26,7 @@
   val output_markup_elem: Markup.T -> (string * string) * string
   val parse_body: string -> XML.body
   val parse: string -> XML.tree
+  val content_of: string -> string
 end;
 
 structure YXML: YXML =
@@ -148,5 +149,7 @@
 
 end;
 
+val content_of = parse_body #> XML.content_of;
+
 end;