equal
deleted
inserted
replaced
961 {pfuns, type_map, env = SOME {vcs, path, ...}} => |
961 {pfuns, type_map, env = SOME {vcs, path, ...}} => |
962 let |
962 let |
963 val (proved, unproved) = partition_vcs vcs; |
963 val (proved, unproved) = partition_vcs vcs; |
964 val _ = Thm.join_proofs (maps (#2 o snd) proved); |
964 val _ = Thm.join_proofs (maps (#2 o snd) proved); |
965 val (proved', proved'') = List.partition (fn (_, (_, thms, _, _)) => |
965 val (proved', proved'') = List.partition (fn (_, (_, thms, _, _)) => |
966 exists (#oracle o Thm.status_of) thms) proved |
966 exists (#oracle o Thm.peek_status) thms) proved |
967 in |
967 in |
968 (if null unproved then () |
968 (if null unproved then () |
969 else (if incomplete then warning else error) |
969 else (if incomplete then warning else error) |
970 (Pretty.string_of (pp_open_vcs unproved)); |
970 (Pretty.string_of (pp_open_vcs unproved)); |
971 if null proved' then () |
971 if null proved' then () |