src/Pure/Isar/outer_syntax.ML
changeset 15156 daa9f645a26e
parent 15144 85929e1b307d
child 15224 1bd35fd87963
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Aug 23 17:06:18 2004 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Aug 23 18:31:18 2004 +0200
     1.3 @@ -296,7 +296,7 @@
     1.4      val pos = Path.position path;
     1.5      val (name', parents, files) = ThyHeader.scan (src, pos);
     1.6      val ml_path = ThyLoad.ml_path name;
     1.7 -    val ml_file = if ml andalso is_some (ThyLoad.check_file ml_path) then [ml_path] else [];
     1.8 +    val ml_file = if ml andalso is_some (ThyLoad.check_file None ml_path) then [ml_path] else [];
     1.9    in
    1.10      if name <> name' then
    1.11        error ("Filename " ^ quote (Path.pack path) ^
    1.12 @@ -315,7 +315,7 @@
    1.13      val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
    1.14      val tr_name = if time then "time_use" else "use";
    1.15    in
    1.16 -    if is_none (ThyLoad.check_file path) then ()
    1.17 +    if is_none (ThyLoad.check_file None path) then ()
    1.18      else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr]
    1.19    end;
    1.20