src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

   let val path = Path.explode file in
     case banner of SOME s => File.write path s | NONE => ();
     xs |> chunk_list 500
        |> List.app (File.append path o space_implode "" o map f)
   end
+  handle IO.Io _ => ()
 
 fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs =
   let
     val (temp_dir, serial) =
       if overlord then (getenv "ISABELLE_HOME_USER", "")

   | _ => ("", [])
 
 fun mash_CLEAR ctxt =
   let val path = mash_model_dir () in
     trace_msg ctxt (K "MaSh CLEAR");
-    File.fold_dir (fn file => fn _ =>
-                      try File.rm (Path.append path (Path.basic file)))
-                  path NONE;
+    try (File.fold_dir (fn file => fn _ =>
+                           try File.rm (Path.append path (Path.basic file)))
+                       path) NONE;
     ()
   end
 
 fun mash_ADD _ _ [] = ()
   | mash_ADD ctxt overlord adds =