--- 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 =