--- a/src/HOL/Tools/Function/function.ML Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Function/function.ML Mon Apr 06 17:06:48 2015 +0200
@@ -286,13 +286,13 @@
(* outer syntax *)
val _ =
- Outer_Syntax.local_theory_to_proof' @{command_spec "function"}
+ Outer_Syntax.local_theory_to_proof' @{command_keyword function}
"define general recursive functions"
(function_parser default_config
>> (fn ((config, fixes), statements) => function_cmd fixes statements config))
val _ =
- Outer_Syntax.local_theory_to_proof @{command_spec "termination"}
+ Outer_Syntax.local_theory_to_proof @{command_keyword termination}
"prove termination of a recursive function"
(Scan.option Parse.term >> termination_cmd)