# 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;