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