src/Pure/Thy/thm_deps.ML
changeset 21858 05f57309170c
parent 21646 c07b5b0e8492
child 24562 fc3cf01e8af1
equal deleted inserted replaced
21857:f9d085c2625c 21858:05f57309170c
    41       in
    41       in
    42         if name <> "" then
    42         if name <> "" then
    43           if not (Symtab.defined gra name) then
    43           if not (Symtab.defined gra name) then
    44             let
    44             let
    45               val (gra', parents') = make_deps_graph prf' (gra, []);
    45               val (gra', parents') = make_deps_graph prf' (gra, []);
    46               val prefx = #1 (Library.split_last (NameSpace.unpack name));
    46               val prefx = #1 (Library.split_last (NameSpace.explode name));
    47               val session =
    47               val session =
    48                 (case prefx of
    48                 (case prefx of
    49                   (x :: _) =>
    49                   (x :: _) =>
    50                     (case ThyInfo.lookup_theory x of
    50                     (case ThyInfo.lookup_theory x of
    51                       SOME thy =>
    51                       SOME thy =>