src/Pure/Thy/thm_deps.ML
changeset 12239 ee360f910ec8
parent 11819 9283b3c11234
child 13530 4813fdc0ef17
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Mon Nov 19 17:40:45 2001 +0100
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Mon Nov 19 17:42:00 2001 +0100
     1.3 @@ -54,7 +54,8 @@
     1.4                      | None => [])
     1.5                   | _ => ["global"]);
     1.6              in
     1.7 -              (Symtab.update ((name,
     1.8 +              if name mem parents' then (gra', parents union parents')
     1.9 +              else (Symtab.update ((name,
    1.10                  {name = Sign.base_name name, ID = name,
    1.11                   dir = space_implode "/" (session @ prefx),
    1.12                   unfold = false, path = "", parents = parents'}), gra'),