src/Pure/Isar/isar_cmd.ML
changeset 16045 6e2c020eed45
parent 16037 13f230daa195
child 16193 05413e43d2f3
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon May 23 13:39:45 2005 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon May 23 14:56:35 2005 +0200
     1.3 @@ -156,8 +156,8 @@
     1.4  
     1.5  (* use ML text *)
     1.6  
     1.7 -fun use path = Toplevel.keep (fn state => ThyInfo.load_file false path) o
     1.8 -  Toplevel.theory (fn thy => (Context.setmp (SOME thy) (ThyInfo.load_file false) path; thy));
     1.9 +fun use path = Toplevel.keep (fn state =>
    1.10 +  Context.setmp (try Toplevel.theory_of state) (ThyInfo.load_file false) path);
    1.11  
    1.12  (*passes changes of theory context*)
    1.13  val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory;