# HG changeset patch
# User wenzelm
# Date 1441205556 -7200
# Node ID d83494bf57ed134329903938583e44abea3688d3
# Parent  896989117ce0d0704ef9f6fdbf2847a04ca7e6d4
trim context for persistent storage;

diff -r 896989117ce0 -r d83494bf57ed src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Wed Sep 02 16:44:17 2015 +0200
+++ b/src/Pure/Isar/calculation.ML	Wed Sep 02 16:52:36 2015 +0200
@@ -74,12 +74,12 @@
 
 val sym_add =
   Thm.declaration_attribute (fn th =>
-    (Data.map o apfst o apsnd) (Thm.add_thm th) #>
+    (Data.map o apfst o apsnd) (Thm.add_thm (Thm.trim_context th)) #>
     Thm.attribute_declaration (Context_Rules.elim_query NONE) th);
 
 val sym_del =
   Thm.declaration_attribute (fn th =>
-    (Data.map o apfst o apsnd) (Thm.del_thm th) #>
+    (Data.map o apfst o apsnd) (Thm.del_thm (Thm.trim_context th)) #>
     Thm.attribute_declaration Context_Rules.rule_del th);