src/Pure/Isar/outer_syntax.ML

   val dest_parsers: unit -> (string * string * string * bool) list
   val print_outer_syntax: unit -> unit
   val add_keywords: string list -> unit
   val add_parsers: parser list -> unit
   val theory_header: token list -> (string * string list * (string * bool) list) * token list
-  val deps_thy: string -> bool -> Path.T -> string list * Path.T list
+  val deps_thy: string -> Path.T -> string list * Path.T list
   val load_thy: string -> bool -> bool -> Path.T -> unit
   val isar: bool -> Toplevel.isar
 end;
 
 structure OuterSyntax: OUTER_SYNTAX =

   P.name -- (P.$$$ "=" |-- P.name -- Scan.repeat (P.$$$ "+" |-- P.name))
   >> (fn (A, (B, Bs)) => (A, B :: Bs, []: (string * bool) list));
 
 end;
 
-fun deps_thy name ml path =
+fun deps_thy name path =
   let
     val src = File.source path;
     val is_old = warn_theory_style path (is_old_theory src);
     val (name', parents, files) =
       (*Note: old style headers dynamically depend on the current lexicon :-( *)
       if is_old then scan_header ThySyn.get_lexicon (Scan.error old_header) src
       else scan_header (K header_lexicon) (Scan.error new_header) src;
 
     val ml_path = ThyLoad.ml_path name;
-    val ml_file = if not ml orelse is_none (ThyLoad.check_file ml_path) then [] else [ml_path];
+    val ml_file = if is_none (ThyLoad.check_file ml_path) then [] else [ml_path];
   in
     if name <> name' then
       error ("Filename " ^ quote (Path.pack path) ^ " does not match theory name " ^ quote name)
     else (parents, map (Path.unpack o #1) files @ ml_file)
   end;