src/Pure/Isar/outer_syntax.ML
changeset 7192 30a67acd0d7e
parent 7104 247e4247b64e
child 7212 1ad29e7d917b
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Aug 06 22:32:27 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Aug 06 22:32:55 1999 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4    val add_keywords: string list -> unit
     1.5    val add_parsers: parser list -> unit
     1.6    val theory_header: token list -> (string * string list * (string * bool) list) * token list
     1.7 -  val deps_thy: string -> bool -> Path.T -> string list * Path.T list
     1.8 +  val deps_thy: string -> Path.T -> string list * Path.T list
     1.9    val load_thy: string -> bool -> bool -> Path.T -> unit
    1.10    val isar: bool -> Toplevel.isar
    1.11  end;
    1.12 @@ -270,7 +270,7 @@
    1.13  
    1.14  end;
    1.15  
    1.16 -fun deps_thy name ml path =
    1.17 +fun deps_thy name path =
    1.18    let
    1.19      val src = File.source path;
    1.20      val is_old = warn_theory_style path (is_old_theory src);
    1.21 @@ -280,7 +280,7 @@
    1.22        else scan_header (K header_lexicon) (Scan.error new_header) src;
    1.23  
    1.24      val ml_path = ThyLoad.ml_path name;
    1.25 -    val ml_file = if not ml orelse is_none (ThyLoad.check_file ml_path) then [] else [ml_path];
    1.26 +    val ml_file = if is_none (ThyLoad.check_file ml_path) then [] else [ml_path];
    1.27    in
    1.28      if name <> name' then
    1.29        error ("Filename " ^ quote (Path.pack path) ^ " does not match theory name " ^ quote name)