src/Pure/Isar/outer_syntax.ML
changeset 20323 ac413d7cc03d
parent 20023 33124a9f5e31
child 21207 cef082634be9
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Aug 03 15:03:09 2006 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Aug 03 15:03:10 2006 +0200
     1.3 @@ -263,14 +263,14 @@
     1.4  local
     1.5  
     1.6  fun try_ml_file name time =
     1.7 -  let
     1.8 -    val path = ThyLoad.ml_path name;
     1.9 -    val tr = Toplevel.imperative (fn () =>
    1.10 -      setmp OldGoals.legacy true (fn () => ThyInfo.load_file time path) ());
    1.11 -    val tr_name = if time then "time_use" else "use";
    1.12 -  in
    1.13 +  let val path = ThyLoad.ml_path name in
    1.14      if is_none (ThyLoad.check_file NONE path) then ()
    1.15 -    else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr]
    1.16 +    else
    1.17 +      let
    1.18 +        val _ = warning ("Loading legacy ML script " ^ quote (Path.pack path));
    1.19 +        val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
    1.20 +        val tr_name = if time then "time_use" else "use";
    1.21 +      in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end
    1.22    end;
    1.23  
    1.24  fun run_thy name path =