--- a/src/HOL/Tools/Function/function.ML Wed Dec 06 19:34:59 2017 +0100
+++ b/src/HOL/Tools/Function/function.ML Wed Dec 06 20:43:09 2017 +0100
@@ -273,13 +273,13 @@
(* outer syntax *)
val _ =
- Outer_Syntax.local_theory_to_proof' @{command_keyword function}
+ Outer_Syntax.local_theory_to_proof' \<^command_keyword>\<open>function\<close>
"define general recursive functions"
(function_parser default_config
>> (fn (config, (fixes, specs)) => function_cmd fixes specs config))
val _ =
- Outer_Syntax.local_theory_to_proof @{command_keyword termination}
+ Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>termination\<close>
"prove termination of a recursive function"
(Scan.option Parse.term >> termination_cmd)