remove obsolete MaSh files
authorblanchet
Sun, 13 Jan 2013 15:04:55 +0100
changeset 50860 e32a283b8ce0
parent 50859 c0f38015a632
child 50861 fa4253914e98
child 50862 5fc8b83322f5
remove obsolete MaSh files
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 () =>