diff -r 39ccdbbed539 -r 5727bcc3c47c src/HOL/Library/old_recdef.ML
--- a/src/HOL/Library/old_recdef.ML	Mon Dec 02 13:34:02 2019 +0100
+++ b/src/HOL/Library/old_recdef.ML	Mon Dec 02 15:04:38 2019 +0100
@@ -2842,7 +2842,7 @@
       |> 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 name Spec_Rules.equational_recdef [lhs] (flat rules)
+      ||> Spec_Rules.add_global (Binding.name bname) Spec_Rules.equational_recdef [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 =