--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Mar 13 17:26:22 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Mar 14 10:08:36 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 []
+ val named_locals = local_facts |> Facts.dest_static [global_facts]
val assms = Assumption.all_assms_of ctxt
fun is_good_unnamed_local th =
not (Thm.has_name_hint th) andalso
@@ -467,14 +467,12 @@
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
- fun add_facts global foldx facts =
+ fun add_facts global foldx =
foldx (fn (name0, ths) => fn accum =>
if name0 <> "" andalso
forall (not o member Thm.eq_thm_prop add_ths) ths andalso
- (Facts.is_concealed facts name0 orelse
+ (Facts.is_concealed local_facts name0 orelse
(not generous andalso is_blacklisted_or_something name0)) then
accum
else
@@ -499,8 +497,7 @@
if name0 = "" then
backquote_thm ctxt th
else
- [Facts.extern ctxt facts name0,
- Name_Space.extern ctxt full_space name0]
+ [Facts.extern ctxt local_facts name0]
|> find_first check_thms
|> the_default name0
|> make_name reserved multi j),
@@ -515,8 +512,8 @@
(* The single-theorem names go before the multiple-theorem ones (e.g.,
"xxx" vs. "xxx(3)"), so that single names are preferred when both are
available. *)
- `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
- |> add_facts true Facts.fold_static global_facts global_facts
+ `I [] |> add_facts false fold (unnamed_locals @ named_locals)
+ |> add_facts true Facts.fold_static global_facts
|> op @
end