--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Dec 03 17:08:39 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Dec 03 17:18:59 2012 +0100
@@ -119,6 +119,7 @@
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
@@ -204,9 +205,9 @@
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