Now handles different theorems with same name more gracefully.
authorberghofe
Mon Nov 19 17:42:00 2001 +0100 (2001-11-19)
changeset 12239ee360f910ec8
parent 12238 09966ccbc84c
child 12240 0760eda193c4
Now handles different theorems with same name more gracefully.
src/Pure/Thy/thm_deps.ML
     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'),