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