changeset 69992 | bd3c10813cc4 |
parent 67713 | 041898537c19 |
child 70494 | 41108e3e9ca5 |
--- a/src/HOL/Tools/Function/function.ML Tue Mar 26 14:23:18 2019 +0100 +++ b/src/HOL/Tools/Function/function.ML Tue Mar 26 22:13:36 2019 +0100 @@ -210,7 +210,7 @@ lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => add_function_data (transform_function_data phi info')) - |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)) + |> Spec_Rules.add Spec_Rules.equational_recdef (fs, tsimps)) end) end in