diff -r 582f54f6b29b -r 1d85ac286c72 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sat Oct 29 00:39:32 2016 +0200
+++ b/src/Pure/Isar/code.ML	Sat Oct 29 00:39:33 2016 +0200
@@ -47,6 +47,7 @@
   val add_eqn: kind * bool -> thm -> theory -> theory
   val add_default_eqn_attribute: kind -> attribute
   val add_default_eqn_attrib: kind -> Token.src
+  val del_eqn_silent: thm -> theory -> theory
   val del_eqn: thm -> theory -> theory
   val del_eqns: string -> theory -> theory
   val del_exception: string -> theory -> theory
@@ -1168,7 +1169,7 @@
     | SOME ((thm, _), SOME tyco) => gen_add_abs_eqn false (thm, tyco) thy
     | NONE => thy;
 
-fun del_eqn thm thy = case mk_eqn Liberal thy (thm, true)
+fun generic_del_eqn strictness thm thy = case mk_eqn strictness thy (thm, true)
  of SOME (thm, _) =>
       let
         fun del_eqn' (Eqns_Default _) = initial_fun_spec
@@ -1180,6 +1181,9 @@
       in change_fun_spec (const_eqn thy thm) del_eqn' thy end
   | NONE => thy;
 
+val del_eqn_silent = generic_del_eqn Silent;
+val del_eqn = generic_del_eqn Liberal;
+
 fun del_eqns c = change_fun_spec c (K None);
 
 fun del_exception c = change_fun_spec c (K (Eqns []));