equal
deleted
inserted
replaced
172 |
172 |
173 val _ = |
173 val _ = |
174 Outer_Syntax.local_theory' @{command_keyword fun} |
174 Outer_Syntax.local_theory' @{command_keyword fun} |
175 "define general recursive functions (short version)" |
175 "define general recursive functions (short version)" |
176 (function_parser fun_config |
176 (function_parser fun_config |
177 >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config)) |
177 >> (fn (config, (fixes, specs)) => add_fun_cmd fixes specs config)) |
178 |
178 |
179 end |
179 end |