# HG changeset patch
# User wenzelm
# Date 1354551539 -3600
# Node ID 6d5dcfb628692773932e8b4b1206dc7760b6ef98
# Parent  dddcaeb92e112908e253b81a9409c9c7c6e4947c# Parent  6be9e490d82a05cf28889f1b3f2437b4eda60e8c
merged

diff -r 6be9e490d82a -r 6d5dcfb62869 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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