--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Jan 24 21:36:21 2015 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Jan 24 21:37:31 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 pstrs : string -> Pretty.T list
val unyxml : string -> string
val pretty_maybe_quote : Keyword.keywords -> Pretty.T -> Pretty.T
val hash_term : term -> int
@@ -281,8 +280,6 @@
val indent_size = 2
-val pstrs = Pretty.breaks o map Pretty.str o space_explode " "
-
val unyxml = ATP_Util.unyxml
val maybe_quote = ATP_Util.maybe_quote