changeset 40169 | 11ea439d947f |
parent 40107 | 374f3ef9f940 |
child 40172 | 008dc2d2c395 |
--- a/src/HOL/Tools/Function/partial_function.ML Tue Oct 26 11:51:09 2010 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Tue Oct 26 12:19:01 2010 +0200 @@ -218,7 +218,7 @@ lthy' |> Local_Theory.note (eq_abinding, [rec_rule]) |-> (fn (_, rec') => - Local_Theory.note ((Binding.qualify true fname (Binding.name "rec"), []), rec')) + Local_Theory.note ((Binding.qualify true fname (Binding.name "simps"), []), rec')) |> snd end;