# HG changeset patch
# User blanchet
# Date 1693920230 -7200
# Node ID de8081bc85a00f9920b49f7d3ddd85b0fa850980
# Parent  a7bcd2af71908705d3e221e22007471a4794d783
tuned Sledgehammer messages

diff -r a7bcd2af7190 -r de8081bc85a0 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Sep 05 15:23:48 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Sep 05 15:23:50 2023 +0200
@@ -262,7 +262,7 @@
           | facts => "The goal is falsified by these facts: " ^ commas facts)
         else
           "Derived \"False\" from these facts alone: " ^
-          commas (map fst used_facts)))
+          space_implode " " (map fst used_facts)))
 
 fun check_expected_outcome ctxt prover_name expect outcome =
   let
@@ -513,7 +513,7 @@
         fun massage_message proof_or_inconsistency s =
           let val s' = strip_time s in
             if member (op =) (Synchronized.value seen_messages) s' then
-              "Found duplicate " ^ proof_or_inconsistency
+              "Duplicate " ^ proof_or_inconsistency
             else
               (Synchronized.change seen_messages (cons s'); s)
           end
diff -r a7bcd2af7190 -r de8081bc85a0 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Sep 05 15:23:48 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Sep 05 15:23:50 2023 +0200
@@ -289,7 +289,8 @@
           val _ =
             if mode = Normal andalso not (is_conjecture_used_in_proof atp_proof)
                andalso not (Logic.get_goal (Thm.prop_of goal) subgoal aconv @{prop False}) then
-              warning ("Derived \"False\" from these facts alone: " ^ commas (map fst used_facts))
+              warning ("Derived \"False\" from these facts alone: " ^
+                space_implode " " (map fst used_facts))
             else
               ()