# HG changeset patch
# User wenzelm
# Date 918056944 -3600
# Node ID 62dc7e9050eb6fc5fe927dc4be4e608ee4cbcf00
# Parent  358f62acf57383a8e4037f138716994cd899e9fc
removed load;
proper use (ThyInfo.load_file);
added use_thy, update_thy;

diff -r 358f62acf573 -r 62dc7e9050eb src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Feb 03 16:48:17 1999 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Feb 03 16:49:04 1999 +0100
@@ -18,7 +18,7 @@
   val cd: string -> Toplevel.transition -> Toplevel.transition
   val pwd: Toplevel.transition -> Toplevel.transition
   val use_thy: string -> Toplevel.transition -> Toplevel.transition
-  val load: string -> Toplevel.transition -> Toplevel.transition
+  val update_thy: string -> Toplevel.transition -> Toplevel.transition
   val print_theory: Toplevel.transition -> Toplevel.transition
   val print_syntax: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
@@ -51,7 +51,7 @@
 
 (* use ML text *)
 
-fun use name = Toplevel.imperative (fn () => Use.use name);
+fun use name = Toplevel.imperative (fn () => ThyInfo.load_file (Path.unpack name));
 
 (*passes changes of theory context*)
 val use_mltext_theory = Toplevel.theory o IsarThy.use_mltext_theory;
@@ -74,10 +74,8 @@
 
 (* load theory files *)
 
-fun use_thy name = Toplevel.imperative (fn () => ThyRead.use_thy name);
-
-fun load name =
-  Toplevel.imperative (fn () => Toplevel.excursion (OuterSyntax.read_file (name ^ ".thy")));
+fun use_thy name = Toplevel.imperative (fn () => ThyInfo.use_thy name);
+fun update_thy name = Toplevel.imperative (fn () => ThyInfo.update_thy name);
 
 
 (* print theory contents *)