# HG changeset patch
# User blanchet
# Date 1358085895 -3600
# Node ID e32a283b8ce0528d3547e717175e74dd1656abb7
# Parent  c0f38015a63254ebf20fd99a31defff042207d0b
remove obsolete MaSh files

diff -r c0f38015a632 -r e32a283b8ce0 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Jan 13 12:28:20 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Jan 13 15:04:55 2013 +0100
@@ -355,7 +355,8 @@
                EQUAL =>
                try_graph ctxt "loading state" Graph.empty (fn () =>
                    fold add_node node_lines Graph.empty)
-             | LESS => Graph.empty (* can't parse old file *)
+             | LESS =>
+               (MaSh.unlearn ctxt; Graph.empty) (* can't parse old file *)
              | GREATER => raise Too_New ()
          in
            trace_msg ctxt (fn () =>