# HG changeset patch
# User blanchet
# Date 1677654051 -3600
# Node ID a15f0fcff04143419cbc9010bb98e43439eda8cf
# Parent  a8458f0df4ee42fdc9b846c6422d6a6a910577f0
don't apply abduction and consistency checking to goals of the form 'False'

diff -r a8458f0df4ee -r a15f0fcff041 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -390,7 +390,7 @@
       @ round_robin (num_slices - num_default_slices) (unknown_provers @ known_provers)
   end
 
-fun prover_slices_of_schedule ctxt factss
+fun prover_slices_of_schedule ctxt goal subgoal factss
     ({abduce, check_consistent, max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases,
       ...} : params)
     schedule =
@@ -420,11 +420,15 @@
         ((slice_size0, abduce0, check_consistent0, num_facts0, fact_filter0), extra) =
       let
         val slice_size = Int.min (max_slice_size, slice_size0)
+        val goal_not_False = not (Logic.get_goal (Thm.prop_of goal) subgoal aconv @{prop False})
         val abduce =
           (case abduce of
-            NONE => abduce0
+            NONE => abduce0 andalso goal_not_False
           | SOME max_candidates => max_candidates > 0)
-        val check_consistent = check_consistent |> the_default check_consistent0
+        val check_consistent =
+          (case check_consistent of
+            NONE => check_consistent0 andalso goal_not_False
+          | SOME check_consistent => check_consistent)
         val fact_filter = fact_filter |> the_default fact_filter0
         val max_facts = max_facts |> the_default num_facts0
         val num_facts = Int.min (max_facts, length (facts_of_filter fact_filter factss))
@@ -549,7 +553,7 @@
             val schedule =
               if mode = Auto_Try then provers
               else schedule_of_provers provers slices
-            val prover_slices = prover_slices_of_schedule ctxt factss params schedule
+            val prover_slices = prover_slices_of_schedule ctxt goal i factss params schedule
 
             val _ =
               if verbose then