# HG changeset patch # User wenzelm # Date 1440948869 -7200 # Node ID add998b3c5973588076310225ed1c5aae140e0f1 # Parent 62f3b498827791c898f3579e62181b84a0fb997b trim context for persistent storage; diff -r 62f3b4988277 -r add998b3c597 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- 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 diff -r 62f3b4988277 -r add998b3c597 src/Pure/Tools/find_theorems.ML --- 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 = diff -r 62f3b4988277 -r add998b3c597 src/Pure/facts.ML --- 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; diff -r 62f3b4988277 -r add998b3c597 src/Pure/global_theory.ML --- 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;