src/HOL/Tools/Function/fun.ML

           |> apsnd (fn Ts => Ts ---> body_type fT)
 
         val qs = map Free (Name.invent Name.context "a" n ~~ argTs)
       in
         HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
-          Const (@{const_name undefined}, rT))
+          Const (\<^const_name>\<open>undefined\<close>, rT))
         |> HOLogic.mk_Trueprop
         |> fold_rev Logic.all qs
       end
   in
     map mk_eqn fixes

 fun add_fun_cmd a b c int = gen_add_fun (fn tac => Function.add_function_cmd a b c tac int)
 
 
 
 val _ =
-  Outer_Syntax.local_theory' @{command_keyword fun}
+  Outer_Syntax.local_theory' \<^command_keyword>\<open>fun\<close>
     "define general recursive functions (short version)"
     (function_parser fun_config
       >> (fn (config, (fixes, specs)) => add_fun_cmd fixes specs config))
 
 end