# HG changeset patch
# User wenzelm
# Date 1694026305 -7200
# Node ID d17fcfd075c39b4374b628299e22de24667ac9b3
# Parent  de8081bc85a00f9920b49f7d3ddd85b0fa850980# Parent  47d0c333d155612015264984e14e91d269a7de9e
merged

diff -r 47d0c333d155 -r d17fcfd075c3 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 06 20:51:28 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 06 20:51:45 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
@@ -464,7 +464,7 @@
   end
 
 fun run_sledgehammer (params as {verbose, spy, provers, falsify, induction_rules, max_facts,
-    max_proofs, slices, ...}) mode writeln_result i (fact_override as {only, ...}) state =
+    max_proofs, slices, timeout, ...}) mode writeln_result i (fact_override as {only, ...}) state =
   if null provers then
     error "No prover is set"
   else
@@ -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
@@ -577,6 +577,8 @@
             val launch = launch_prover_and_preplay params mode has_already_found_something
               found_something massage_message writeln_result learn
 
+            val timer = Timer.startRealTimer ()
+
             val schedule =
               if mode = Auto_Try then provers
               else schedule_of_provers provers slices
@@ -597,7 +599,8 @@
             else
               (learn chained_thms;
                Par_List.map (fn (prover, slice) =>
-                   if Synchronized.value found_proofs_and_falsifications < max_proofs then
+                   if Synchronized.value found_proofs_and_falsifications < max_proofs
+                      andalso Timer.checkRealTimer timer < timeout then
                      launch problem slice prover
                    else
                      (SH_None, ""))
diff -r 47d0c333d155 -r d17fcfd075c3 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Sep 06 20:51:28 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Sep 06 20:51:45 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
               ()