# HG changeset patch
# User wenzelm
# Date 934921188 -7200
# Node ID 886ecd6a27ac793d672be2db745bb50c35f52268
# Parent  f17f2e8ba0c76214165f49bd9440f1c55f6340e9
ThyInfo.may_load_file;

diff -r f17f2e8ba0c7 -r 886ecd6a27ac src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Aug 17 22:19:25 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Aug 17 22:19:48 1999 +0200
@@ -286,10 +286,10 @@
 fun try_ml_file name ml time =
   let
     val path = ThyLoad.ml_path name;
-    val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
+    val tr = Toplevel.imperative (fn () => ThyInfo.may_load_file ml time path);
     val tr_name = if time then "time_use" else "use";
   in
-    if not ml orelse is_none (ThyLoad.check_file path) then ()
+    if is_none (ThyLoad.check_file path) then ()
     else Toplevel.excursion_error [Toplevel.empty |> Toplevel.name tr_name |> tr]
   end;