--- a/src/HOL/Library/old_recdef.ML Tue Mar 26 14:23:18 2019 +0100
+++ b/src/HOL/Library/old_recdef.ML Tue Mar 26 22:13:36 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 Spec_Rules.Equational ([lhs], flat rules)
+ ||> Spec_Rules.add_global 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 =