--- 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