changeset 7786 | cf9d07ad62af |
parent 7785 | c06825c396e8 |
child 7853 | a4acf1b4d5a8 |
--- a/src/Pure/Thy/thm_deps.ML Thu Oct 07 14:44:55 1999 +0200 +++ b/src/Pure/Thy/thm_deps.ML Thu Oct 07 15:40:32 1999 +0200 @@ -58,7 +58,7 @@ | None => []) | _ => ["global"]) in - (Symtab.update_new ((name, + (Symtab.update ((name, {name = Sign.base_name name, ID = name, dir = space_implode "/" (session @ prefx), unfold = false, path = "", parents = parents'}), gra'), name ins parents)