changeset 59936 | b8ffc3dc9e24 |
parent 59627 | bb1e4a35d506 |
child 60682 | 5a6cd2560549 |
--- a/src/HOL/Tools/Function/fun.ML Mon Apr 06 16:30:44 2015 +0200 +++ b/src/HOL/Tools/Function/fun.ML Mon Apr 06 17:06:48 2015 +0200 @@ -172,7 +172,7 @@ val _ = - Outer_Syntax.local_theory' @{command_spec "fun"} + Outer_Syntax.local_theory' @{command_keyword fun} "define general recursive functions (short version)" (function_parser fun_config >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))