src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML

          fact_count global_facts >= max_facts_for_complex_check then
         K false
       else
         is_too_complex
     val local_facts = Proof_Context.facts_of ctxt
-    val named_locals = local_facts |> Facts.dest_static [global_facts]
+    val named_locals = local_facts |> Facts.dest_static true [global_facts]
     val assms = Assumption.all_assms_of ctxt
     fun is_good_unnamed_local th =
       not (Thm.has_name_hint th) andalso
       forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
     val unnamed_locals =