# HG changeset patch
# User huffman
# Date 1268533008 28800
# Node ID 7de1e14d9277017b0654091a9dfc594c22d2c5e2
# Parent  8b3327bcbf7d807d1d3e10bb7131e3fbacdf1647
fixpat command prints legacy_feature warning

diff -r 8b3327bcbf7d -r 7de1e14d9277 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Sat Mar 13 17:36:53 2010 -0800
+++ b/src/HOLCF/Tools/fixrec.ML	Sat Mar 13 18:16:48 2010 -0800
@@ -422,6 +422,7 @@
 
 fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
   let
+    val _ = legacy_feature "\"fixpat\"; prefer \"fixrec_simp\" method instead";
     val atts = map (prep_attrib thy) srcs;
     val ts = map (prep_term thy) strings;
     val simps = map (fix_pat thy) ts;