--- a/src/HOL/Tools/Function/function.ML Wed Dec 29 18:18:42 2010 +0100
+++ b/src/HOL/Tools/Function/function.ML Wed Dec 29 21:52:41 2010 +0100
@@ -85,11 +85,15 @@
val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
val defname = mk_defname fixes
- val FunctionConfig {partials, tailrec, ...} = config
+ val FunctionConfig {partials, tailrec, default, ...} = config
val _ =
if tailrec then Output.legacy_feature
"'function (tailrec)' command. Use 'partial_function (tailrec)'."
else ()
+ val _ =
+ if is_some default then Output.legacy_feature
+ "'function (default)'. Use 'partial_function'."
+ else ()
val ((goal_state, cont), lthy') =
Function_Mutual.prepare_function_mutual config defname fixes eqs lthy