src/Pure/Thy/thm_deps.ML
changeset 24562 fc3cf01e8af1
parent 21858 05f57309170c
child 26138 dc578de1d3e9
equal deleted inserted replaced
24561:7b4aa14d2491 24562:fc3cf01e8af1
    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 =>
    52                         let val name = #name (Present.get_info thy)
    52                         let val name = Present.session_name thy
    53                         in if name = "" then [] else [name] end
    53                         in if name = "" then [] else [name] end
    54                     | NONE => [])
    54                     | NONE => [])
    55                  | _ => ["global"]);
    55                  | _ => ["global"]);
    56             in
    56             in
    57               if member (op =) parents' name then (gra', parents union parents')
    57               if member (op =) parents' name then (gra', parents union parents')