# HG changeset patch
# User blanchet
# Date 1678445812 -3600
# Node ID d39027e1c8c52644c6da379c14f23f0e471a59b1
# Parent  e5b09ff7d72f9c3607493e36665ada3cfc81cc06
don't try to falisfy goals with schematics

diff -r e5b09ff7d72f -r d39027e1c8c5 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Mar 09 14:29:46 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Mar 10 11:56:52 2023 +0100
@@ -419,7 +419,8 @@
         ((slice_size0, abduce0, falsify0, 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 the_subgoal = Logic.get_goal (Thm.prop_of goal) subgoal
+        val goal_not_False = not (the_subgoal aconv @{prop False})
         val abduce =
           (case abduce of
             NONE => abduce0 andalso goal_not_False
@@ -428,6 +429,7 @@
           (case falsify of
             NONE => falsify0 andalso goal_not_False
           | SOME falsify => falsify)
+          andalso not (Term.is_schematic the_subgoal)
         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))