# HG changeset patch
# User wenzelm
# Date 1129911295 -7200
# Node ID a77862a93f025f01be0edf2201f3cd7e7832956d
# Parent  5b54db4a44ee5c93f1156585691dbf0fc1adff74
load_file: setmp OldGoals.legacy true;

diff -r 5b54db4a44ee -r a77862a93f02 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Oct 21 18:14:54 2005 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Oct 21 18:14:55 2005 +0200
@@ -261,7 +261,8 @@
 fun try_ml_file name time =
   let
     val path = ThyLoad.ml_path name;
-    val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
+    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
     if is_none (ThyLoad.check_file NONE path) then ()