Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use_thy, update_thy: Context.save;
authorwenzelm
Fri, 05 Feb 1999 21:03:06 +0100
changeset 6243 fb293dfa2df3
parent 6242 3d75f5a99f60
child 6244 daecd68ecc8c
use_thy, update_thy: Context.save;
src/Pure/Isar/isar_cmd.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle