src/Pure/Thy/thm_deps.ML

                       | session => [session])
                   | NONE => [])
                | _ => ["global"]);
             val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
             val entry =
-              {name = Sign.base_name name,
+              {name = NameSpace.base_name name,
                ID = name,
                dir = space_implode "/" (session @ prefix),
                unfold = false,
                path = "",
                parents = parents};