simplified ThyLoad.deps_thy etc.: discontinued attached ML files;

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Aug 08 23:07:47 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Aug 08 23:07:48 2007 +0200
@@ -692,14 +692,14 @@
 
         fun filerefs f =
             let val thy = thy_name f
-                val filerefs = #uses (ThyLoad.deps_thy (Path.dir f) thy true)
+                val filerefs = #uses (ThyLoad.deps_thy (Path.dir f) thy)
             in
                 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
                                      name=NONE, idtables=[], fileurls=filerefs})
             end
 
         fun thyrefs thy =
-            let val thyrefs = #imports (ThyLoad.deps_thy Path.current thy true)
+            let val thyrefs = #imports (ThyLoad.deps_thy Path.current thy)
             in
                 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
                                      name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,

--- a/src/Pure/Thy/thy_load.ML	Wed Aug 08 23:07:47 2007 +0200
+++ b/src/Pure/Thy/thy_load.ML	Wed Aug 08 23:07:48 2007 +0200
@@ -24,19 +24,18 @@
   val thy_path: string -> Path.T
   val check_file: Path.T -> Path.T -> (Path.T * File.ident) option
   val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
-  val check_thy: Path.T -> string -> bool -> (Path.T * File.ident) * (Path.T * File.ident) option
-  val deps_thy: Path.T -> string -> bool ->
-   {master: (Path.T * File.ident) * (Path.T * File.ident) option,
-    text: string list, imports: string list, uses: Path.T list}
+  val check_thy: Path.T -> string -> Path.T * File.ident
+  val deps_thy: Path.T -> string ->
+   {master: Path.T * File.ident, text: string list, imports: string list, uses: Path.T list}
   val load_ml: Path.T -> Path.T -> Path.T * File.ident
-  val load_thy: Path.T -> string -> Position.T -> string list -> bool -> bool -> unit
+  val load_thy: Path.T -> string -> Position.T -> string list -> bool -> unit
 end;
 
 signature PRIVATE_THY_LOAD =
 sig
   include THY_LOAD
   (*this backdoor is sealed later*)
-  val load_thy_fn: (Path.T -> string -> Position.T -> string list -> bool -> bool -> unit) ref
+  val load_thy_fn: (Path.T -> string -> Position.T -> string list -> bool -> unit) ref
 end;
 
 structure ThyLoad: PRIVATE_THY_LOAD =
@@ -88,7 +87,7 @@
 fun check_file dir path = check_ext [] (search_path dir path) dir path;
 fun check_ml dir path = check_ext ml_exts (search_path dir path) dir path;
 
-fun check_thy dir name ml =
+fun check_thy dir name =
   let
     val thy_file = thy_path name;
     val paths = search_path dir thy_file;
@@ -96,25 +95,22 @@
     (case check_ext [] paths dir thy_file of
       NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
         " in " ^ commas_quote (map Path.implode paths))
-    | SOME thy_id => (thy_id, if ml then check_file dir (ml_path name) else NONE))
+    | SOME thy_id => thy_id)
   end;
 
 
 (* theory deps *)
 
-fun deps_thy dir name ml =
+fun deps_thy dir name =
   let
-    val master as ((path, _), _) = check_thy dir name ml;
+    val master as (path, _) = check_thy dir name;
     val text = explode (File.read path);
     val (name', imports, uses) =
       ThyHeader.read (Position.path path) (Source.of_list_limited 8000 text);
     val _ = name = name' orelse
       error ("Filename " ^ quote (Path.implode (Path.base path)) ^
         " does not agree with theory name " ^ quote name');
-    val ml_file =
-      if ml andalso is_some (check_file dir (ml_path name))
-      then [ml_path name] else [];
-    val uses = map (Path.explode o #1) uses @ ml_file;
+    val uses = map (Path.explode o #1) uses;
   in {master = master, text = text, imports = imports, uses = uses} end;
 
 
@@ -127,8 +123,8 @@
 
 (*dependent on outer syntax*)
 val load_thy_fn =
-  ref (undefined: Path.T -> string -> Position.T -> string list -> bool -> bool -> unit);
-fun load_thy dir name pos text ml time = ! load_thy_fn dir name pos text ml time;
+  ref (undefined: Path.T -> string -> Position.T -> string list -> bool -> unit);
+fun load_thy dir name pos text time = ! load_thy_fn dir name pos text time;
 
 end;