changeset 43277 | 1fd31f859fc7 |
parent 42361 | 23f352990944 |
child 44052 | 00f0c8782a51 |
--- a/src/HOL/Tools/Function/function.ML Wed Jun 08 15:25:44 2011 +0200 +++ b/src/HOL/Tools/Function/function.ML Wed Jun 08 15:39:55 2011 +0200 @@ -87,8 +87,7 @@ val defname = mk_defname fixes val FunctionConfig {partials, default, ...} = config val _ = - if is_some default then Output.legacy_feature - "'function (default)'. Use 'partial_function'." + if is_some default then legacy_feature "'function (default)'. Use 'partial_function'." else () val ((goal_state, cont), lthy') =