changeset 40172 | 008dc2d2c395 |
parent 40169 | 11ea439d947f |
child 40180 | c3ef007115a0 |
--- a/src/HOL/Tools/Function/partial_function.ML Tue Oct 26 12:19:01 2010 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Tue Oct 26 12:19:02 2010 +0200 @@ -218,7 +218,8 @@ 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;