--- a/src/HOL/TPTP/MaSh_Eval.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy Sat Jan 05 17:24:33 2019 +0100
@@ -23,7 +23,7 @@
\<close>
ML \<open>
-val params = Sledgehammer_Commands.default_params @{theory} []
+val params = Sledgehammer_Commands.default_params \<^theory> []
val prob_dir = prefix ^ "mash_problems"
\<close>
@@ -36,7 +36,7 @@
ML \<open>
if do_it then
- evaluate_mash_suggestions @{context} params range (SOME prob_dir)
+ evaluate_mash_suggestions \<^context> params range (SOME prob_dir)
[prefix ^ "mepo_suggestions",
prefix ^ "mash_suggestions",
prefix ^ "mash_prover_suggestions",