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