src/Pure/Thy/thm_deps.ML

               val prefx = #1 (Library.split_last (NameSpace.unpack name));
               val session =
                 (case prefx of
                   (x :: _) =>
                     (case ThyInfo.lookup_theory x of
-                      Some thy =>
+                      SOME thy =>
                         let val name = #name (Present.get_info thy)
                         in if name = "" then [] else [name] end 
-                    | None => [])
+                    | NONE => [])
                  | _ => ["global"]);
             in
               if name mem parents' then (gra', parents union parents')
               else (Symtab.update ((name,
                 {name = Sign.base_name name, ID = name,