# HG changeset patch
# User haftmann
# Date 1268231362 -3600
# Node ID 863bee3a91535a333e3f6731eddda4c2f53c75b9
# Parent  c3bef0c972d7cc219d9c630a3a0b1e6614806323
recdef is legacy

diff -r c3bef0c972d7 -r 863bee3a9153 src/HOL/Tools/recdef.ML
--- 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;