diff -r f9e4a9621c75 -r 20e76da3a0ef src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Aug 28 19:07:10 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Aug 28 20:05:39 2014 +0200
@@ -31,6 +31,7 @@
   val maybe_instantiate_inducts : Proof.context -> term list -> term ->
     (((unit -> string) * 'a) * thm) list -> (((unit -> string) * 'a) * thm) list
   val fact_of_raw_fact : raw_fact -> fact
+  val is_useful_unnamed_local_fact : Proof.context -> thm -> bool
 
   val all_facts : Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list ->
     status Termtab.table -> raw_fact list
@@ -442,6 +443,18 @@
 
 fun fact_count facts = Facts.fold_static (K (Integer.add 1)) facts 0
 
+fun is_useful_unnamed_local_fact ctxt =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val global_facts = Global_Theory.facts_of thy
+    val local_facts = Proof_Context.facts_of ctxt
+    val named_locals = Facts.dest_static true [global_facts] local_facts
+  in
+    fn th =>
+      not (Thm.has_name_hint th) andalso
+      forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
+  end
+
 fun all_facts ctxt generous ho_atp reserved add_ths chained css =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -450,16 +463,13 @@
       if generous orelse 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 true [global_facts]
     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
+      |> filter (is_useful_unnamed_local_fact ctxt)
+      |> map (pair "" o single)
 
-    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 =
-      union Thm.eq_thm_prop (Facts.props local_facts) chained
-      |> filter is_good_unnamed_local |> map (pair "" o single)
     val full_space = Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
     val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp