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