# HG changeset patch # User wenzelm # Date 1709980532 -3600 # Node ID ce3a0d2c9aa793108a172a85e94a7dc8929d0c28 # Parent 60f1e32792c158d44a1b96c33e5549db0dc056c9 eliminate odd aliases (see also 2746dfc9ceae); diff -r 60f1e32792c1 -r ce3a0d2c9aa7 src/HOL/Tools/Nitpick/nitpick_util.ML --- 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 diff -r 60f1e32792c1 -r ce3a0d2c9aa7 src/HOL/ex/Sketch_and_Explore.thy --- 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 @@ \ \TODO pointless to annotate explicit fixes in term\ |> 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