--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sun Aug 30 17:32:50 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sun Aug 30 17:34:29 2015 +0200
@@ -460,6 +460,7 @@
fun all_facts ctxt generous ho_atp keywords add_ths chained css =
let
val thy = Proof_Context.theory_of ctxt
+ val transfer = Global_Theory.transfer_theories thy;
val global_facts = Global_Theory.facts_of thy
val is_too_complex =
if generous orelse fact_count global_facts >= max_facts_for_complex_check then K false
@@ -493,35 +494,37 @@
NONE => false
| SOME ths' => eq_list Thm.eq_thm_prop (ths, ths'))
in
- snd (fold_rev (fn th => fn (j, accum) =>
- (j - 1,
- if not (member Thm.eq_thm_prop add_ths th) andalso
- (is_likely_tautology_too_meta_or_too_technical th orelse
- is_too_complex (Thm.prop_of th)) then
- accum
- else
- let
- fun get_name () =
- if name0 = "" orelse name0 = local_thisN then
- backquote_thm ctxt th
- else
- let val short_name = Facts.extern ctxt facts name0 in
- if check_thms short_name then
- short_name
- else
- let val long_name = Name_Space.extern ctxt full_space name0 in
- if check_thms long_name then
- long_name
- else
- name0
- end
- end
- |> make_name keywords multi j
- val stature = stature_of_thm global assms chained css name0 th
- val new = ((get_name, stature), th)
- in
- (if multi then apsnd else apfst) (cons new) accum
- end)) ths (n, accum))
+ snd (fold_rev (fn th0 => fn (j, accum) =>
+ let val th = transfer th0 in
+ (j - 1,
+ if not (member Thm.eq_thm_prop add_ths th) andalso
+ (is_likely_tautology_too_meta_or_too_technical th orelse
+ is_too_complex (Thm.prop_of th)) then
+ accum
+ else
+ let
+ fun get_name () =
+ if name0 = "" orelse name0 = local_thisN then
+ backquote_thm ctxt th
+ else
+ let val short_name = Facts.extern ctxt facts name0 in
+ if check_thms short_name then
+ short_name
+ else
+ let val long_name = Name_Space.extern ctxt full_space name0 in
+ if check_thms long_name then
+ long_name
+ else
+ name0
+ end
+ end
+ |> make_name keywords multi j
+ val stature = stature_of_thm global assms chained css name0 th
+ val new = ((get_name, stature), th)
+ in
+ (if multi then apsnd else apfst) (cons new) accum
+ end)
+ end) ths (n, accum))
end)
in
(* The single-theorem names go before the multiple-theorem ones (e.g., "xxx" vs. "xxx(3)"), so
--- a/src/Pure/Tools/find_theorems.ML Sun Aug 30 17:32:50 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML Sun Aug 30 17:34:29 2015 +0200
@@ -380,12 +380,15 @@
fun all_facts_of ctxt =
let
+ val thy = Proof_Context.theory_of ctxt;
+ val transfer = Global_Theory.transfer_theories thy;
val local_facts = Proof_Context.facts_of ctxt;
- val global_facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);
+ val global_facts = Global_Theory.facts_of thy;
in
- maps Facts.selections
- (Facts.dest_static false [global_facts] local_facts @
- Facts.dest_static false [] global_facts)
+ (Facts.dest_static false [global_facts] local_facts @
+ Facts.dest_static false [] global_facts)
+ |> maps Facts.selections
+ |> map (apsnd transfer)
end;
fun filter_theorems ctxt theorems query =
--- a/src/Pure/facts.ML Sun Aug 30 17:32:50 2015 +0200
+++ b/src/Pure/facts.ML Sun Aug 30 17:34:29 2015 +0200
@@ -228,11 +228,12 @@
fun add_static context {strict, index} (b, ths) (Facts {facts, props}) =
let
+ val ths' = map Thm.trim_context ths;
val (name, facts') =
if Binding.is_empty b then ("", facts)
- else Name_Space.define context strict (b, Static ths) facts;
+ else Name_Space.define context strict (b, Static ths') facts;
val props' = props
- |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths;
+ |> index ? fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths';
in (name, make_facts facts' props') end;
--- a/src/Pure/global_theory.ML Sun Aug 30 17:32:50 2015 +0200
+++ b/src/Pure/global_theory.ML Sun Aug 30 17:34:29 2015 +0200
@@ -14,6 +14,7 @@
val hide_fact: bool -> string -> theory -> theory
val get_thms: theory -> xstring -> thm list
val get_thm: theory -> xstring -> thm
+ val transfer_theories: theory -> thm -> thm
val all_thms_of: theory -> bool -> (string * thm) list
val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list
@@ -77,12 +78,22 @@
fun get_thm thy xname =
Facts.the_single (xname, Position.none) (get_thms thy xname);
+fun transfer_theories thy =
+ let
+ val theories =
+ fold (fn thy' => Symtab.update (Context.theory_name thy', thy'))
+ (Theory.nodes_of thy) Symtab.empty;
+ fun transfer th =
+ Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_name_of_thm th))) th;
+ in transfer end;
+
fun all_thms_of thy verbose =
let
+ val transfer = transfer_theories thy;
val facts = facts_of thy;
fun add (name, ths) =
if not verbose andalso Facts.is_concealed facts name then I
- else append (map (`(Thm.get_name_hint)) ths);
+ else append (map (`(Thm.get_name_hint) o transfer) ths);
in Facts.fold_static add facts [] end;