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