# HG changeset patch
# User wenzelm
# Date 1441294338 -7200
# Node ID 8ed21464e260b4ca128e3e35a7a419d3a3031cc8
# Parent  0ec9fd8d8119524420a84c808b361547163a4464
trim context for persistent storage;

diff -r 0ec9fd8d8119 -r 8ed21464e260 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Thu Sep 03 17:14:57 2015 +0200
+++ b/src/HOL/Tools/typedef.ML	Thu Sep 03 17:32:18 2015 +0200
@@ -65,10 +65,15 @@
   fun merge data = Symtab.merge_list (K true) data;
 );
 
-val get_info = Symtab.lookup_list o Data.get o Context.Proof;
-val get_info_global = Symtab.lookup_list o Data.get o Context.Theory;
+fun get_info_generic context =
+  Symtab.lookup_list (Data.get context) #>
+  map (transform_info (Morphism.transfer_morphism (Context.theory_of context)));
 
-fun put_info name info = Data.map (Symtab.cons_list (name, info));
+val get_info = get_info_generic o Context.Proof;
+val get_info_global = get_info_generic o Context.Theory;
+
+fun put_info name info =
+  Data.map (Symtab.cons_list (name, transform_info Morphism.trim_context_morphism info));
 
 
 (* global interpretation *)
@@ -289,4 +294,3 @@
     >> (fn ((((vs, t), mx), A), morphs) => fn lthy => typedef_cmd ((t, vs, mx), A, morphs) lthy));
 
 end;
-