# HG changeset patch
# User wenzelm
# Date 1441223594 -7200
# Node ID 2b7ef52a4ea9aca013425a6435299e0a80de8f4b
# Parent  16f7f9aa4263b38ec0838ff1ec7a12ae7011b078
trim context for persistent storage;

diff -r 16f7f9aa4263 -r 2b7ef52a4ea9 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Wed Sep 02 20:14:19 2015 +0200
+++ b/src/Pure/Isar/local_defs.ML	Wed Sep 02 21:53:14 2015 +0200
@@ -178,8 +178,8 @@
   Pretty.writeln (Pretty.big_list "definitional rewrite rules:"
     (map (Display.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
 
-val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
-val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);
+val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm o Thm.trim_context);
+val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm o Thm.trim_context);
 
 
 (* meta rewrite rules *)