diff -r 56a87a5093be -r cd935b7cb3fb src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Library/old_recdef.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -2834,7 +2834,7 @@
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
     val simp_att =
       if null tcs then [Simplifier.simp_add,
-        Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute Code.Equation]
+        Named_Theorems.add @{named_theorems nitpick_simp}]
       else [];
     val ((simps' :: rules', [induct']), thy2) =
       Proof_Context.theory_of ctxt1
@@ -2842,7 +2842,8 @@
       |> Global_Theory.add_thmss
         (((Binding.name "simps", flat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
       ||>> Global_Theory.add_thms [((Binding.name "induct", induct), [])]
-      ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules);
+      ||> Spec_Rules.add_global Spec_Rules.Equational ([lhs], flat rules)
+      ||> null tcs ? Code.declare_default_eqns_global (map (rpair true) (flat rules));
     val result = {lhs = lhs, simps = simps', rules = rules', induct = induct', tcs = tcs};
     val thy3 =
       thy2