# HG changeset patch
# User wenzelm
# Date 1518802124 -3600
# Node ID 5cca859b2d2e15669a52a103bf2a1d9944f81e6d
# Parent  cfa71f9933f430cc3ab320e3557c60e3ec8e6d66
trim context of persistent data;
no need to trim context for del operations;

diff -r cfa71f9933f4 -r 5cca859b2d2e src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Fri Feb 16 18:26:13 2018 +0100
+++ b/src/Pure/Isar/bundle.ML	Fri Feb 16 18:28:44 2018 +0100
@@ -55,9 +55,10 @@
 val get_bundle = get_bundle_generic o Context.Proof;
 fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt;
 
-fun define_bundle def context =
+fun define_bundle (b, bundle) context =
   let
-    val (name, bundles') = Name_Space.define context true def (get_bundles_generic context);
+    val bundle' = Attrib.trim_context bundle;
+    val (name, bundles') = Name_Space.define context true (b, bundle') (get_bundles_generic context);
     val context' = (Data.map o apfst o K) bundles' context;
   in (name, context') end;
 
@@ -70,7 +71,7 @@
   | NONE => error "Missing bundle target");
 
 val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE;
-val set_target = Context.theory_map o Data.map o apsnd o K o SOME;
+val set_target = Context.theory_map o Data.map o apsnd o K o SOME o Attrib.trim_context;
 
 fun augment_target thms =
   Local_Theory.background_theory (fn thy => set_target (the_target thy @ thms) thy);
diff -r cfa71f9933f4 -r 5cca859b2d2e src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Fri Feb 16 18:26:13 2018 +0100
+++ b/src/Pure/Isar/calculation.ML	Fri Feb 16 18:28:44 2018 +0100
@@ -98,8 +98,11 @@
 
 (* add/del rules *)
 
-val trans_add = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.update);
-val trans_del = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove);
+val trans_add =
+  Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.update o Thm.trim_context);
+
+val trans_del =
+  Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove);
 
 val sym_add =
   Thm.declaration_attribute (fn th =>
@@ -108,7 +111,7 @@
 
 val sym_del =
   Thm.declaration_attribute (fn th =>
-    (Data.map o apfst o apsnd) (Thm.del_thm (Thm.trim_context th)) #>
+    (Data.map o apfst o apsnd) (Thm.del_thm th) #>
     Thm.attribute_declaration Context_Rules.rule_del th);
 
 
diff -r cfa71f9933f4 -r 5cca859b2d2e src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Fri Feb 16 18:26:13 2018 +0100
+++ b/src/Pure/Isar/local_defs.ML	Fri Feb 16 18:28:44 2018 +0100
@@ -189,7 +189,7 @@
     (map (Thm.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
 
 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);
+val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);
 
 
 (* meta rewrite rules *)