recdef is legacy

--- 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;