--- 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);