equal
deleted
inserted
replaced
59 (fn thy => |
59 (fn thy => |
60 let |
60 let |
61 val thyname = get_generating_thy thy |
61 val thyname = get_generating_thy thy |
62 val segname = get_import_segment thy |
62 val segname = get_import_segment thy |
63 val (int_thms,facts) = Replay.setup_int_thms thyname thy |
63 val (int_thms,facts) = Replay.setup_int_thms thyname thy |
64 val thmnames = List.filter (not o should_ignore thyname thy) facts |
64 val thmnames = filter_out (should_ignore thyname thy) facts |
65 fun replay thy = |
65 fun replay thy = |
66 let |
66 let |
67 val _ = ImportRecorder.load_history thyname |
67 val _ = ImportRecorder.load_history thyname |
68 val thy = Replay.import_thms thyname int_thms thmnames thy |
68 val thy = Replay.import_thms thyname int_thms thmnames thy |
69 handle x => (ImportRecorder.save_history thyname; raise x) |
69 handle x => (ImportRecorder.save_history thyname; raise x) |