# HG changeset patch
# User wenzelm
# Date 1440965275 -7200
# Node ID 07e5c6c71206cde80df998faa4c6fc5b4687aa2d
# Parent  5f6a1e31f3adb198cfb4bfb122c8b1e7cb279837
trim context for persistent storage;

diff -r 5f6a1e31f3ad -r 07e5c6c71206 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sun Aug 30 21:26:42 2015 +0200
+++ b/src/Tools/induct.ML	Sun Aug 30 22:07:55 2015 +0200
@@ -203,8 +203,6 @@
 fun filter_rules (rs: rules) th =
   filter (fn (_, th') => Thm.eq_thm_prop (th, th')) (Item_Net.content rs);
 
-fun lookup_rule (rs: rules) = AList.lookup (op =) (Item_Net.content rs);
-
 fun pretty_rules ctxt kind rs =
   let val thms = map snd (Item_Net.content rs)
   in Pretty.big_list kind (map (Display.pretty_thm_item ctxt) thms) end;
@@ -261,16 +259,24 @@
 
 (* access rules *)
 
-val lookup_casesT = lookup_rule o #1 o #1 o get_local;
-val lookup_casesP = lookup_rule o #2 o #1 o get_local;
-val lookup_inductT = lookup_rule o #1 o #2 o get_local;
-val lookup_inductP = lookup_rule o #2 o #2 o get_local;
-val lookup_coinductT = lookup_rule o #1 o #3 o get_local;
-val lookup_coinductP = lookup_rule o #2 o #3 o get_local;
+local
 
+fun lookup_rule which ctxt =
+  AList.lookup (op =) (Item_Net.content (which (get_local ctxt)))
+  #> Option.map (Thm.transfer (Proof_Context.theory_of ctxt));
 
 fun find_rules which how ctxt x =
-  map snd (Item_Net.retrieve (which (get_local ctxt)) (how x));
+  Item_Net.retrieve (which (get_local ctxt)) (how x)
+  |> map (Thm.transfer (Proof_Context.theory_of ctxt) o snd);
+
+in
+
+val lookup_casesT = lookup_rule (#1 o #1);
+val lookup_casesP = lookup_rule (#2 o #1);
+val lookup_inductT = lookup_rule (#1 o #2);
+val lookup_inductP = lookup_rule (#2 o #2);
+val lookup_coinductT = lookup_rule (#1 o #3);
+val lookup_coinductP = lookup_rule (#2 o #3);
 
 val find_casesT = find_rules (#1 o #1) Net.encode_type;
 val find_casesP = find_rules (#2 o #1) I;
@@ -279,6 +285,8 @@
 val find_coinductT = find_rules (#1 o #3) Net.encode_type;
 val find_coinductP = find_rules (#2 o #3) I;
 
+end;
+
 
 
 (** attributes **)
@@ -289,7 +297,7 @@
   Thm.mixed_attribute (fn (context, thm) =>
     let
       val thm' = g thm;
-      val context' = Data.map (f (name, thm')) context;
+      val context' = Data.map (f (name, Thm.trim_context thm')) context;
     in (context', thm') end);
 
 fun del_att which =