src/Pure/Thy/thm_deps.ML
changeset 15531 08c8dad8e399
parent 14981 e73f8140af78
child 15570 8d8c70b41bab
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -47,10 +47,10 @@
     1.4                  (case prefx of
     1.5                    (x :: _) =>
     1.6                      (case ThyInfo.lookup_theory x of
     1.7 -                      Some thy =>
     1.8 +                      SOME thy =>
     1.9                          let val name = #name (Present.get_info thy)
    1.10                          in if name = "" then [] else [name] end 
    1.11 -                    | None => [])
    1.12 +                    | NONE => [])
    1.13                   | _ => ["global"]);
    1.14              in
    1.15                if name mem parents' then (gra', parents union parents')