use: not a theory command!
authorwenzelm
Mon May 23 14:56:35 2005 +0200 (2005-05-23 ago)
changeset 160456e2c020eed45
parent 16044 6887e6d12a94
child 16046 7d68cd1b1b8b
use: not a theory command!
src/Pure/Isar/isar_cmd.ML
     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;