src/HOL/TPTP/mash_export.ML

   generate_mepo_or_mash_suggestions
     (fn ctxt => fn _ => fn params => fn max_suggs => fn hyp_ts => fn concl_t =>
        not (Config.get ctxt Sledgehammer_MaSh.duplicates) ? Sledgehammer_Fact.drop_duplicate_facts
        #> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
 
-fun generate_mash_suggestions algorithm =
+fun generate_mash_suggestions algorithm ctxt =
   (Options.put_default @{system_option MaSh} algorithm;
-   Sledgehammer_MaSh.mash_unlearn ();
+   Sledgehammer_MaSh.mash_unlearn ctxt;
    generate_mepo_or_mash_suggestions
      (fn ctxt => fn thy_name => fn params as {provers = prover :: _, ...} =>
           fn max_suggs => fn hyp_ts => fn concl_t =>
         tap (Sledgehammer_MaSh.mash_learn_facts ctxt params prover 2 false
           Sledgehammer_Util.one_year)
         #> Sledgehammer_MaSh.mash_suggested_facts ctxt thy_name params max_suggs hyp_ts concl_t
-        #> fst))
+        #> fst) ctxt)
 
 fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name mesh_file_name =
   let
     val mesh_path = Path.explode mesh_file_name
     val _ = File.write mesh_path ""