src/HOL/Tools/value_command.ML

       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   in Pretty.writeln p end;
 
 val opt_modes =
-  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
+  Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\<open>)\<close>)) [];
 
 val opt_evaluator =
-  Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
+  Scan.option (\<^keyword>\<open>[\<close> |-- Parse.name --| \<^keyword>\<open>]\<close>)
   
 val _ =
-  Outer_Syntax.command @{command_keyword value} "evaluate and print term"
+  Outer_Syntax.command \<^command_keyword>\<open>value\<close> "evaluate and print term"
     (opt_evaluator -- opt_modes -- Parse.term
       >> (fn ((some_name, modes), t) => Toplevel.keep (value_cmd some_name modes t)));
 
 val _ = Theory.setup
-  (Thy_Output.antiquotation @{binding value}
+  (Thy_Output.antiquotation \<^binding>\<open>value\<close>
     (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
     (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
       (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
         [style (value_maybe_select some_name context t)]))
   #> add_evaluator ("simp", Code_Simp.dynamic_value)