--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Mar 15 10:29:42 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Mar 15 11:22:25 2014 +0100
@@ -459,7 +459,7 @@
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