# HG changeset patch # User wenzelm # Date 1440970464 -7200 # Node ID a2c6f7f64aca34b3429c1bf489734264ee843413 # Parent 0306e209fa9e01ae12e0094306e4faaa40e7c0bb trim context for persistent storage; diff -r 0306e209fa9e -r a2c6f7f64aca src/Pure/Isar/spec_rules.ML --- 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;