equal
deleted
inserted
replaced
57 if member (op =) parents' name then (gra', parents union parents') |
57 if member (op =) parents' name then (gra', parents union parents') |
58 else (Symtab.update (name, |
58 else (Symtab.update (name, |
59 {name = Sign.base_name name, ID = name, |
59 {name = Sign.base_name name, ID = name, |
60 dir = space_implode "/" (session @ prefx), |
60 dir = space_implode "/" (session @ prefx), |
61 unfold = false, path = "", parents = parents'}) gra', |
61 unfold = false, path = "", parents = parents'}) gra', |
62 name ins parents) |
62 insert (op =) name parents) |
63 end |
63 end |
64 else (gra, name ins parents) |
64 else (gra, insert (op =) name parents) |
65 else |
65 else |
66 make_deps_graph prf' (gra, parents) |
66 make_deps_graph prf' (gra, parents) |
67 end); |
67 end); |
68 |
68 |
69 fun thm_deps thms = |
69 fun thm_deps thms = |