# HG changeset patch
# User krauss
# Date 1293449601 -3600
# Node ID 05bd42fdaea8780e2995bc36c326c742d0266158
# Parent  aae9f912cca8f6bbf46f3a3cf5131bd29465e1e2
function (tailrec) is a legacy feature

diff -r aae9f912cca8 -r 05bd42fdaea8 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sat Dec 25 22:18:58 2010 +0100
+++ b/src/HOL/Tools/Function/function.ML	Mon Dec 27 12:33:21 2010 +0100
@@ -85,7 +85,11 @@
     val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
 
     val defname = mk_defname fixes
-    val FunctionConfig {partials, ...} = config
+    val FunctionConfig {partials, tailrec, ...} = config
+    val _ =
+      if tailrec then Output.legacy_feature
+        "'function (tailrec)' command. Use 'partial_function (tailrec)'."
+      else ()
 
     val ((goal_state, cont), lthy') =
       Function_Mutual.prepare_function_mutual config defname fixes eqs lthy