trim context for persistent storage;

--- a/src/Pure/Isar/spec_rules.ML	Sun Aug 30 22:58:26 2015 +0200
+++ b/src/Pure/Isar/spec_rules.ML	Sun Aug 30 23:34:24 2015 +0200
@@ -21,7 +21,7 @@
 structure Spec_Rules: SPEC_RULES =
 struct
 
-(* maintain rules *)
+(* rules *)
 
 datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive;
 type spec = rough_classification * (term list * thm list);
@@ -40,11 +40,30 @@
   val merge = Item_Net.merge;
 );
 
-val get = Item_Net.content o Rules.get o Context.Proof;
-val get_global = Item_Net.content o Rules.get o Context.Theory;
+
+(* get *)
+
+fun get_generic context =
+  let
+    val thy = Context.theory_of context;
+    val transfer = Global_Theory.transfer_theories thy;
+  in Item_Net.content (Rules.get context) |> (map o apsnd o apsnd o map) transfer end;
+
+val get = get_generic o Context.Proof;
+val get_global = get_generic o Context.Theory;
 
-val retrieve = Item_Net.retrieve o Rules.get o Context.Proof;
-val retrieve_global = Item_Net.retrieve o Rules.get o Context.Theory;
+
+(* retrieve *)
+
+fun retrieve_generic context =
+  Item_Net.retrieve (Rules.get context)
+  #> (map o apsnd o apsnd o map) (Thm.transfer (Context.theory_of context));
+
+val retrieve = retrieve_generic o Context.Proof;
+val retrieve_global = retrieve_generic o Context.Theory;
+
+
+(* add *)
 
 fun add class (ts, ths) lthy =
   let
@@ -56,11 +75,12 @@
           val (ts', ths') =
             Morphism.fact phi (map Drule.mk_term cts @ ths)
             |> chop (length cts)
-            |>> map (Thm.term_of o Drule.dest_term);
+            |>> map (Thm.term_of o Drule.dest_term)
+            ||> map Thm.trim_context;
         in Rules.map (Item_Net.update (class, (ts', ths'))) end)
   end;
 
 fun add_global class spec =
-  Context.theory_map (Rules.map (Item_Net.update (class, spec)));
+  Context.theory_map (Rules.map (Item_Net.update (class, (apsnd o map) Thm.trim_context spec)));
 
 end;