src/Pure/Thy/thm_deps.ML
changeset 17224 a78339014063
parent 17020 f3014afac46f
child 17412 e26cb20ef0cc
equal deleted inserted replaced
17223:430edc6b7826 17224:a78339014063
    53                         in if name = "" then [] else [name] end
    53                         in if name = "" then [] else [name] end
    54                     | NONE => [])
    54                     | NONE => [])
    55                  | _ => ["global"]);
    55                  | _ => ["global"]);
    56             in
    56             in
    57               if name mem parents' then (gra', parents union parents')
    57               if name mem parents' then (gra', parents union parents')
    58               else (Symtab.update ((name,
    58               else (Symtab.curried_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                name ins parents)
    63             end
    63             end
    64           else (gra, name ins parents)
    64           else (gra, name ins parents)
    65         else
    65         else
    66           make_deps_graph prf' (gra, parents)
    66           make_deps_graph prf' (gra, parents)