--- a/src/HOL/Tools/try0.ML Wed Dec 06 19:34:59 2017 +0100
+++ b/src/HOL/Tools/try0.ML Wed Dec 06 20:43:09 2017 +0100
@@ -182,11 +182,11 @@
|| Scan.repeat parse_attr >> (fn quad => fold merge_attrs quad ([], [], [], []))) x;
val _ =
- Outer_Syntax.command @{command_keyword try0} "try a combination of proof methods"
+ Outer_Syntax.command \<^command_keyword>\<open>try0\<close> "try a combination of proof methods"
(Scan.optional parse_attrs ([], [], [], []) #>> try0_trans);
fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []);
-val _ = Try.tool_setup (try0N, (30, @{system_option auto_methods}, try_try0));
+val _ = Try.tool_setup (try0N, (30, \<^system_option>\<open>auto_methods\<close>, try_try0));
end;