# 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 () =>