# HG changeset patch
# User haftmann
# Date 1268231363 -3600
# Node ID d9c9b81b16a80221c271fbae795b2e10b41ac3f5
# Parent  863bee3a91535a333e3f6731eddda4c2f53c75b9
constdefs is legacy

diff -r 863bee3a9153 -r d9c9b81b16a8 src/Pure/Isar/constdefs.ML
--- 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;