src/Pure/Thy/thm_deps.ML
changeset 21858 05f57309170c
parent 21646 c07b5b0e8492
child 24562 fc3cf01e8af1
--- a/src/Pure/Thy/thm_deps.ML	Thu Dec 14 22:19:39 2006 +0100
+++ b/src/Pure/Thy/thm_deps.ML	Fri Dec 15 00:08:06 2006 +0100
@@ -43,7 +43,7 @@
           if not (Symtab.defined gra name) then
             let
               val (gra', parents') = make_deps_graph prf' (gra, []);
-              val prefx = #1 (Library.split_last (NameSpace.unpack name));
+              val prefx = #1 (Library.split_last (NameSpace.explode name));
               val session =
                 (case prefx of
                   (x :: _) =>