src/HOL/Tools/Function/partial_function.ML

           THEN resolve_tac lthy' @{thms refl} 1)
       end;
     val ((_, [rec_rule']), lthy'') = lthy' |> Local_Theory.note (eq_abinding, [rec_rule])
   in
     lthy''
-    |> Spec_Rules.add Spec_Rules.Equational ([f], [rec_rule'])
+    |> Spec_Rules.add Spec_Rules.equational_recdef ([f], [rec_rule'])
     |> note_qualified ("simps", [rec_rule'])
     |> note_qualified ("mono", [mono_thm])
     |> (case raw_induct of NONE => I | SOME thm => note_qualified ("raw_induct", [thm]))
     |> note_qualified ("fixp_induct", [specialized_fixp_induct])
     |> pair (f, rec_rule')