src/Pure/Thy/thm_deps.ML
changeset 15531 08c8dad8e399
parent 14981 e73f8140af78
child 15570 8d8c70b41bab
--- a/src/Pure/Thy/thm_deps.ML	Fri Feb 11 18:51:00 2005 +0100
+++ b/src/Pure/Thy/thm_deps.ML	Sun Feb 13 17:15:14 2005 +0100
@@ -47,10 +47,10 @@
                 (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')