1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Oct 21 18:14:54 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Oct 21 18:14:55 2005 +0200
     1.3 @@ -261,7 +261,8 @@
     1.4  fun try_ml_file name time =
     1.5    let
     1.6      val path = ThyLoad.ml_path name;
     1.7 -    val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
     1.8 +    val tr = Toplevel.imperative (fn () =>
     1.9 +      setmp OldGoals.legacy true (fn () => ThyInfo.load_file time path) ());
    1.10      val tr_name = if time then "time_use" else "use";
    1.11    in
    1.12      if is_none (ThyLoad.check_file NONE path) then ()