--- 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 ()