changeset 44052 | 00f0c8782a51 |
parent 43277 | 1fd31f859fc7 |
child 44192 | a32ca9165928 |
--- a/src/HOL/Tools/Function/function.ML Mon Aug 08 13:19:19 2011 +0200 +++ b/src/HOL/Tools/Function/function.ML Mon Aug 08 13:29:54 2011 +0200 @@ -87,7 +87,8 @@ val defname = mk_defname fixes val FunctionConfig {partials, default, ...} = config val _ = - if is_some default then legacy_feature "'function (default)'. Use 'partial_function'." + if is_some default + then legacy_feature "\"function (default)\" -- use 'partial_function' instead" else () val ((goal_state, cont), lthy') =