constdefs is legacy

--- a/src/Pure/Isar/constdefs.ML	Wed Mar 10 15:29:22 2010 +0100
+++ b/src/Pure/Isar/constdefs.ML	Wed Mar 10 15:29:23 2010 +0100
@@ -22,6 +22,8 @@
 fun gen_constdef prep_vars prep_prop prep_att
     structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
   let
+    val _ = legacy_feature ("\"constdefs\"; prefer \"definition\" instead");
+
     fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
 
     val thy_ctxt = ProofContext.init thy;