src/Pure/Thy/thy_info.ML

 
 
 (* thy database *)
 
 type deps =
- {master: (Path.T * File.ident),  (*master dependencies for thy file*)
-  imports: string list};          (*source specification of imports (partially qualified)*)
+ {master: (Path.T * Thy_Load.file_ident),  (*master dependencies for thy file*)
+  imports: string list};  (*source specification of imports (partially qualified)*)
 
 fun make_deps master imports : deps = {master = master, imports = imports};
 
 fun master_dir (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d);
 fun base_name s = Path.implode (Path.base (Path.explode s));