--- a/src/HOL/TPTP/mash_export.ML Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/TPTP/mash_export.ML Sat Jan 05 17:24:33 2019 +0100
@@ -287,7 +287,7 @@
#> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
fun generate_mash_suggestions algorithm ctxt =
- (Options.put_default @{system_option MaSh} algorithm;
+ (Options.put_default \<^system_option>\<open>MaSh\<close> algorithm;
Sledgehammer_MaSh.mash_unlearn ctxt;
generate_mepo_or_mash_suggestions
(fn ctxt => fn thy_name => fn params as {provers = prover :: _, ...} =>