src/Pure/Thy/thy_info.ML

--- a/src/Pure/Thy/thy_info.ML	Thu Jul 22 20:46:45 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Jul 22 22:31:20 2010 +0200
@@ -296,11 +296,7 @@
   let
     val dir = master_directory name;
     val _ = check_unfinished error name;
-  in
-    (case Thy_Load.check_file dir path of
-      SOME path_info => change_deps name (provide path name path_info)
-    | NONE => error ("Could not find file " ^ quote (Path.implode path)))
-  end;
+  in change_deps name (provide path name (Thy_Load.check_file dir path)) end;
 
 fun load_file path =
   if ! Output.timing then
@@ -417,12 +413,12 @@
 
 local
 
-fun check_ml master (src_path, info) =
+fun check_file master (src_path, info) =
   let val info' =
     (case info of
       NONE => NONE
     | SOME (_, id) =>
-        (case Thy_Load.check_ml (master_dir master) src_path of
+        (case Thy_Load.test_file (master_dir master) src_path of
           NONE => NONE
         | SOME (path', id') => if id <> id' then NONE else SOME (path', id')))
   in (src_path, info') end;
@@ -444,7 +440,7 @@
           in (false, init_deps master' text' parents' files', parents') end
         else
           let
-            val files' = map (check_ml master') files;
+            val files' = map (check_file master') files;
             val current = update_time >= 0 andalso can get_theory name
               andalso forall (is_some o snd) files';
             val update_time' = if current then update_time else ~1;