src/Pure/Thy/thm_deps.ML
changeset 20854 f9cf9e62d11c
parent 20664 ffbc5a57191a
child 21646 c07b5b0e8492
equal deleted inserted replaced
20853:3ff5a2e05810 20854:f9cf9e62d11c
    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 =