use_thy, update_thy: Context.save;
authorwenzelm
Fri Feb 05 21:03:06 1999 +0100 (1999-02-05 ago)
changeset 6243fb293dfa2df3
parent 6242 3d75f5a99f60
child 6244 daecd68ecc8c
use_thy, update_thy: Context.save;
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Feb 05 21:02:17 1999 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Feb 05 21:03:06 1999 +0100
     1.3 @@ -51,7 +51,7 @@
     1.4  
     1.5  (* use ML text *)
     1.6  
     1.7 -fun use name = Toplevel.imperative (fn () => ThyInfo.load_file (Path.unpack name));
     1.8 +fun use name = Toplevel.imperative (fn () => ThyInfo.use name);
     1.9  
    1.10  (*passes changes of theory context*)
    1.11  val use_mltext_theory = Toplevel.theory o IsarThy.use_mltext_theory;
    1.12 @@ -74,8 +74,8 @@
    1.13  
    1.14  (* load theory files *)
    1.15  
    1.16 -fun use_thy name = Toplevel.imperative (fn () => ThyInfo.use_thy name);
    1.17 -fun update_thy name = Toplevel.imperative (fn () => ThyInfo.update_thy name);
    1.18 +fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name);
    1.19 +fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name);
    1.20  
    1.21  
    1.22  (* print theory contents *)