# HG changeset patch
# User blanchet
# Date 1677835810 -3600
# Node ID 615a6a6a4b0b44098b87e90e90f215bd9db23dcd
# Parent  57ede1743caf9327ddbb3c0f2eec8e240b8afa74
got rid of 'important message' mechanism in SystemOnTPTP (which is less used nowadays)

diff -r 57ede1743caf -r 615a6a6a4b0b src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Mar 02 17:46:29 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Mar 03 10:30:10 2023 +0100
@@ -68,7 +68,6 @@
 
   val short_output : bool -> string -> string
   val string_of_atp_failure : atp_failure -> string
-  val extract_important_message : string -> string
   val extract_known_atp_failure : (atp_failure * string) list -> string -> atp_failure option
   val extract_tstplike_proof_and_outcome :
     bool -> (string * string) list -> (atp_failure * string) list -> string
@@ -202,17 +201,6 @@
     | NONE => "")
   | NONE => "")
 
-val tstp_important_message_delims =
-  ("% SZS start RequiredInformation", "% SZS end RequiredInformation")
-
-fun extract_important_message output =
-  (case extract_delimited tstp_important_message_delims output of
-    "" => ""
-  | s => s |> space_explode "\n" |> filter_out (curry (op =) "")
-           |> map (perhaps (try (unprefix "%")))
-           |> map (perhaps (try (unprefix " ")))
-           |> space_implode "\n " |> quote)
-
 (* Splits by the first possible of a list of delimiters. *)
 fun extract_tstplike_proof delims output =
   (case apply2 (find_first (fn s => String.isSubstring s output)) (ListPair.unzip delims) of
diff -r 57ede1743caf -r 615a6a6a4b0b src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Mar 02 17:46:29 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Mar 03 10:30:10 2023 +0100
@@ -98,9 +98,6 @@
   | suffix_of_mode MaSh = ""
   | suffix_of_mode Minimize = "_min"
 
-(* Important messages are important but not so important that users want to see them each time. *)
-val important_message_keep_quotient = 25
-
 fun run_atp mode name
     ({debug, verbose, overlord, abduce = abduce_max_candidates, strict, max_mono_iters,
       max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, slices, timeout,
@@ -284,11 +281,6 @@
          (format, type_enc)) =
       with_cleanup clean_up run () |> tap export
 
-    val important_message =
-      if mode = Normal andalso Random.random_range 0 (important_message_keep_quotient - 1) = 0
-      then extract_important_message output
-      else ""
-
     val (outcome, used_facts, preferred_methss, message) =
       (case outcome of
         NONE =>
@@ -342,11 +334,7 @@
                 val num_chained = length (#facts (Proof.goal state))
               in
                 proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
-                  one_line_params ^
-                (if important_message <> "" then
-                   "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
-                 else
-                   "")
+                  one_line_params
               end)
         end
       | SOME failure =>