changeset 20854 | f9cf9e62d11c |
parent 20664 | ffbc5a57191a |
child 21646 | c07b5b0e8492 |
--- a/src/Pure/Thy/thm_deps.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/Pure/Thy/thm_deps.ML Wed Oct 04 14:17:38 2006 +0200 @@ -59,9 +59,9 @@ {name = Sign.base_name name, ID = name, dir = space_implode "/" (session @ prefx), unfold = false, path = "", parents = parents'}) gra', - name ins parents) + insert (op =) name parents) end - else (gra, name ins parents) + else (gra, insert (op =) name parents) else make_deps_graph prf' (gra, parents) end);