src/HOL/Tools/Function/partial_function.ML

         THEN rtac @{thm refl} 1) end;
   in
     lthy'
     |> Local_Theory.note (eq_abinding, [rec_rule])
     |-> (fn (_, rec') =>
-      Local_Theory.note ((Binding.qualify true fname (Binding.name "simps"), []), rec'))
+      Spec_Rules.add Spec_Rules.Equational ([f], [rec'])
+      |> Local_Theory.note ((Binding.qualify true fname (Binding.name "simps"), []), rec'))
     |> snd
   end;
 
 val add_partial_function = gen_add_partial_function Specification.check_spec;
 val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;