--- a/src/HOL/Tools/functor.ML Wed Dec 06 19:34:59 2017 +0100
+++ b/src/HOL/Tools/functor.ML Wed Dec 06 20:43:09 2017 +0100
@@ -275,8 +275,8 @@
val functor_cmd = gen_functor Syntax.read_term;
val _ =
- Outer_Syntax.local_theory_to_proof @{command_keyword functor}
+ Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>functor\<close>
"register operations managing the functorial structure of a type"
- (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term >> uncurry functor_cmd);
+ (Scan.option (Parse.name --| \<^keyword>\<open>:\<close>) -- Parse.term >> uncurry functor_cmd);
end;