| changeset 35690 | 863bee3a9153 |
| parent 34956 | fac9d0311725 |
| child 35756 | cfde251d03a5 |
--- a/src/HOL/Tools/recdef.ML Wed Mar 10 15:29:22 2010 +0100 +++ b/src/HOL/Tools/recdef.ML Wed Mar 10 15:29:22 2010 +0100 @@ -184,6 +184,7 @@ fun gen_add_recdef tfl_fn prep_att prep_hints not_permissive raw_name R eq_srcs hints thy = let + val _ = legacy_feature ("\"recdef\"; prefer \"function\" instead"); val _ = requires_recdef thy; val name = Sign.intern_const thy raw_name;