1.1 --- a/src/Pure/Thy/thm_deps.ML	Wed Oct 04 14:14:33 2006 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Wed Oct 04 14:17:38 2006 +0200
     1.3 @@ -59,9 +59,9 @@
     1.4                  {name = Sign.base_name name, ID = name,
     1.5                   dir = space_implode "/" (session @ prefx),
     1.6                   unfold = false, path = "", parents = parents'}) gra',
     1.7 -               name ins parents)
     1.8 +               insert (op =) name parents)
     1.9              end
    1.10 -          else (gra, name ins parents)
    1.11 +          else (gra, insert (op =) name parents)
    1.12          else
    1.13            make_deps_graph prf' (gra, parents)
    1.14        end);