# HG changeset patch
# User wenzelm
# Date 1154610190 -7200
# Node ID ac413d7cc03d82d20e0d87b658e61a7fd5a5bdc7
# Parent  c80539928948ca685209100219a98833b726a3c9
removed OldGoals.legacy flag (always warn);
added warning for legacy ML scripts;

diff -r c80539928948 -r ac413d7cc03d src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Aug 03 15:03:09 2006 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Aug 03 15:03:10 2006 +0200
@@ -263,14 +263,14 @@
 local
 
 fun try_ml_file name time =
-  let
-    val path = ThyLoad.ml_path name;
-    val tr = Toplevel.imperative (fn () =>
-      setmp OldGoals.legacy true (fn () => ThyInfo.load_file time path) ());
-    val tr_name = if time then "time_use" else "use";
-  in
+  let val path = ThyLoad.ml_path name in
     if is_none (ThyLoad.check_file NONE path) then ()
-    else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr]
+    else
+      let
+        val _ = warning ("Loading legacy ML script " ^ quote (Path.pack 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
   end;
 
 fun run_thy name path =