--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Mar 09 11:05:32 2024 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Sat Mar 09 11:35:32 2024 +0100
@@ -277,11 +277,9 @@
val indent_size = 2
-val maybe_quote = ATP_Util.maybe_quote
-
fun pretty_maybe_quote ctxt pretty =
let val s = Pretty.unformatted_string_of pretty
- in if maybe_quote ctxt s = s then pretty else Pretty.quote pretty end
+ in if ATP_Util.maybe_quote ctxt s = s then pretty else Pretty.quote pretty end
val hashw = ATP_Util.hashw
val hashw_string = ATP_Util.hashw_string
--- a/src/HOL/ex/Sketch_and_Explore.thy Sat Mar 09 11:05:32 2024 +0100
+++ b/src/HOL/ex/Sketch_and_Explore.thy Sat Mar 09 11:35:32 2024 +0100
@@ -17,13 +17,10 @@
val concl = Logic.strip_imp_concl horn;
in (fixes, assms, concl) end;
-fun maybe_quote ctxt =
- ATP_Util.maybe_quote ctxt;
-
fun print_typ ctxt T =
T
|> Syntax.string_of_typ ctxt
- |> maybe_quote ctxt;
+ |> ATP_Util.maybe_quote ctxt;
fun print_term ctxt t =
t
@@ -32,7 +29,7 @@
\<comment> \<open>TODO pointless to annotate explicit fixes in term\<close>
|> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
|> Sledgehammer_Util.simplify_spaces
- |> maybe_quote ctxt;
+ |> ATP_Util.maybe_quote ctxt;
fun eigen_context_for_statement (fixes, assms, concl) ctxt =
let