# HG changeset patch
# User wenzelm
# Date 918244986 -3600
# Node ID fb293dfa2df3a545215e843b1c01f11b120510e1
# Parent  3d75f5a99f60a91b7e22c13eb08b27746e27b3c1
use_thy, update_thy: Context.save;

diff -r 3d75f5a99f60 -r fb293dfa2df3 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Feb 05 21:02:17 1999 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Feb 05 21:03:06 1999 +0100
@@ -51,7 +51,7 @@
 
 (* use ML text *)
 
-fun use name = Toplevel.imperative (fn () => ThyInfo.load_file (Path.unpack name));
+fun use name = Toplevel.imperative (fn () => ThyInfo.use name);
 
 (*passes changes of theory context*)
 val use_mltext_theory = Toplevel.theory o IsarThy.use_mltext_theory;
@@ -74,8 +74,8 @@
 
 (* load theory files *)
 
-fun use_thy name = Toplevel.imperative (fn () => ThyInfo.use_thy name);
-fun update_thy name = Toplevel.imperative (fn () => ThyInfo.update_thy name);
+fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name);
+fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name);
 
 
 (* print theory contents *)