# HG changeset patch # User wenzelm # Date 1440932880 -7200 # Node ID 0d401f8749422186c6028a82f8b2d48efc32ec83 # Parent 408ff239053085172c9ab1399205813157514f75 trim context for persistent storage; diff -r 408ff2390530 -r 0d401f874942 src/Provers/classical.ML --- a/src/Provers/classical.ML Sun Aug 30 12:17:23 2015 +0200 +++ b/src/Provers/classical.ML Sun Aug 30 13:08:00 2015 +0200 @@ -915,9 +915,9 @@ fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) => let - val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt; + val [rules1, rules2, rules4] = Context_Rules.find_rules ctxt false facts goal; val {extra_netpair, ...} = rep_claset_of ctxt; - val rules3 = Context_Rules.find_rules_netpair true facts goal extra_netpair; + val rules3 = Context_Rules.find_rules_netpair ctxt true facts goal extra_netpair; val rules = rules1 @ rules2 @ rules3 @ rules4; val ruleq = Drule.multi_resolves (SOME ctxt) facts rules; val _ = Method.trace ctxt rules; diff -r 408ff2390530 -r 0d401f874942 src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Sun Aug 30 12:17:23 2015 +0200 +++ b/src/Pure/Isar/context_rules.ML Sun Aug 30 13:08:00 2015 +0200 @@ -11,8 +11,8 @@ val netpair_bang: Proof.context -> netpair val netpair: Proof.context -> netpair val orderlist: ((int * int) * 'a) list -> 'a list - val find_rules_netpair: bool -> thm list -> term -> netpair -> thm list - val find_rules: bool -> thm list -> term -> Proof.context -> thm list list + val find_rules_netpair: Proof.context -> bool -> thm list -> term -> netpair -> thm list + val find_rules: Proof.context -> bool -> thm list -> term -> thm list list val print_rules: Proof.context -> unit val addSWrapper: (Proof.context -> (int -> tactic) -> int -> tactic) -> theory -> theory val addWrapper: (Proof.context -> (int -> tactic) -> int -> tactic) -> theory -> theory @@ -76,9 +76,12 @@ Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers}; fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) = - let val w = (case opt_w of SOME w => w | NONE => Tactic.subgoals_of_brl (b, th)) in - make_rules (next - 1) ((w, ((i, b), th)) :: rules) - (nth_map i (Tactic.insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers + let + val w = (case opt_w of SOME w => w | NONE => Tactic.subgoals_of_brl (b, th)); + val th' = Thm.trim_context th; + in + make_rules (next - 1) ((w, ((i, b), th')) :: rules) + (nth_map i (Tactic.insert_tagged_brl ((w, next), (b, th'))) netpairs) wrappers end; fun del_rule0 th (rs as Rules {next, rules, netpairs, wrappers}) = @@ -144,6 +147,8 @@ fun orderlist_no_weight brls = untaglist (sort (int_ord o apply2 (snd o fst)) brls); +local + fun may_unify weighted t net = map snd ((if weighted then orderlist else orderlist_no_weight) (Net.unify_term net t)); @@ -152,11 +157,16 @@ fun find_irules w goal = may_unify w (Logic.strip_assums_concl goal); -fun find_rules_netpair weighted facts goal (inet, enet) = - find_erules weighted facts enet @ find_irules weighted goal inet; +in -fun find_rules weighted facts goal = - map (find_rules_netpair weighted facts goal) o netpairs; +fun find_rules_netpair ctxt weighted facts goal (inet, enet) = + find_erules weighted facts enet @ find_irules weighted goal inet + |> map (Thm.transfer (Proof_Context.theory_of ctxt)); + +fun find_rules ctxt weighted facts goal = + map (find_rules_netpair ctxt weighted facts goal) (netpairs ctxt); + +end; (* wrappers *) diff -r 408ff2390530 -r 0d401f874942 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Sun Aug 30 12:17:23 2015 +0200 +++ b/src/Pure/Isar/method.ML Sun Aug 30 13:08:00 2015 +0200 @@ -239,7 +239,7 @@ let val rules = if not (null arg_rules) then arg_rules - else flat (Context_Rules.find_rules false facts goal ctxt) + else flat (Context_Rules.find_rules ctxt false facts goal); in trace ctxt rules; tac ctxt rules facts i end); fun meth tac x y = METHOD (HEADGOAL o tac x y); diff -r 408ff2390530 -r 0d401f874942 src/Pure/Tools/named_theorems.ML --- a/src/Pure/Tools/named_theorems.ML Sun Aug 30 12:17:23 2015 +0200 +++ b/src/Pure/Tools/named_theorems.ML Sun Aug 30 13:08:00 2015 +0200 @@ -50,10 +50,12 @@ fun member ctxt = Item_Net.member o the_entry (Context.Proof ctxt); -fun content context = rev o Item_Net.content o the_entry context; +fun content context = + rev o map (Thm.transfer (Context.theory_of context)) o Item_Net.content o the_entry context; + val get = content o Context.Proof; -fun add_thm name = map_entry name o Item_Net.update; +fun add_thm name th = map_entry name (Item_Net.update (Thm.trim_context th)); fun del_thm name = map_entry name o Item_Net.remove; val add = Thm.declaration_attribute o add_thm;