src/Pure/Isar/outer_syntax.ML
changeset 7243 886ecd6a27ac
parent 7212 1ad29e7d917b
child 7333 6cb15c6f1d9f
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Aug 17 22:19:25 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Aug 17 22:19:48 1999 +0200
     1.3 @@ -286,10 +286,10 @@
     1.4  fun try_ml_file name ml time =
     1.5    let
     1.6      val path = ThyLoad.ml_path name;
     1.7 -    val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
     1.8 +    val tr = Toplevel.imperative (fn () => ThyInfo.may_load_file ml time path);
     1.9      val tr_name = if time then "time_use" else "use";
    1.10    in
    1.11 -    if not ml orelse is_none (ThyLoad.check_file path) then ()
    1.12 +    if is_none (ThyLoad.check_file path) then ()
    1.13      else Toplevel.excursion_error [Toplevel.empty |> Toplevel.name tr_name |> tr]
    1.14    end;
    1.15