src/Pure/Isar/outer_syntax.ML
changeset 22826 0f4c501a691e
parent 22120 8424ef945cb5
child 23679 57dceb84d1a0
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Apr 30 13:22:35 2007 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Apr 30 13:32:58 2007 +0200
     1.3 @@ -268,7 +268,7 @@
     1.4      if is_none (ThyLoad.check_file NONE path) then ()
     1.5      else
     1.6        let
     1.7 -        val _ = warning ("Loading legacy ML script " ^ quote (Path.implode path));
     1.8 +        val _ = legacy_feature ("loading attached ML script " ^ quote (Path.implode path));
     1.9          val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
    1.10          val tr_name = if time then "time_use" else "use";
    1.11        in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end