--- a/src/Pure/Isar/outer_syntax.ML Mon Apr 30 13:22:35 2007 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Mon Apr 30 13:32:58 2007 +0200
@@ -268,7 +268,7 @@
if is_none (ThyLoad.check_file NONE path) then ()
else
let
- val _ = warning ("Loading legacy ML script " ^ quote (Path.implode path));
+ val _ = legacy_feature ("loading attached ML script " ^ quote (Path.implode path));
val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
val tr_name = if time then "time_use" else "use";
in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end