# HG changeset patch
# User wenzelm
# Date 1440968306 -7200
# Node ID 0306e209fa9e01ae12e0094306e4faaa40e7c0bb
# Parent  07e5c6c71206cde80df998faa4c6fc5b4687aa2d
trim context for persistent storage;

diff -r 07e5c6c71206 -r 0306e209fa9e src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sun Aug 30 22:07:55 2015 +0200
+++ b/src/Pure/more_thm.ML	Sun Aug 30 22:58:26 2015 +0200
@@ -583,8 +583,11 @@
   fun merge _ = empty;
 );
 
-fun register_proofs more_thms = Proofs.map (fn thms => fold cons more_thms thms);
-val join_theory_proofs = Thm.join_proofs o rev o Proofs.get;
+fun register_proofs more_thms =
+  Proofs.map (fold (cons o Thm.trim_context) more_thms);
+
+fun join_theory_proofs thy =
+  Thm.join_proofs (map (Thm.transfer thy) (rev (Proofs.get thy)));
 
 
 open Thm;
@@ -593,4 +596,3 @@
 
 structure Basic_Thm: BASIC_THM = Thm;
 open Basic_Thm;
-