# HG changeset patch
# User blanchet
# Date 1701863157 -3600
# Node ID 4a4db49e6d0517bada76ca632634d08c0567758f
# Parent  7529588b3daf8379179f3ce1da0d0ab2948ac1bc
include unnamed chained facts in Sledgehammer's relevance filter

diff -r 7529588b3daf -r 4a4db49e6d05 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 06 12:45:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 06 12:45:57 2023 +0100
@@ -464,8 +464,7 @@
     val assms = Assumption.all_assms_of ctxt
     val named_locals = Facts.dest_static true [global_facts] local_facts
     val unnamed_locals =
-      Facts.props local_facts
-      |> map #1
+      chained @ map #1 (Facts.props local_facts)
       |> filter (is_useful_unnamed_local_fact ctxt)
       |> map (pair "" o single)