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