# HG changeset patch
# User wenzelm
# Date 918056976 -3600
# Node ID f9fdb4e297903cda82897478c4b3a70f021def94
# Parent  62dc7e9050eb6fc5fe927dc4be4e608ee4cbcf00
removed load;
added update_thy;

diff -r 62dc7e9050eb -r f9fdb4e29790 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Feb 03 16:49:04 1999 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Feb 03 16:49:36 1999 +0100
@@ -464,12 +464,12 @@
     (Scan.succeed IsarCmd.pwd);
 
 val use_thyP =
-  OuterSyntax.parser true "use_thy" "use_thy theory file"
+  OuterSyntax.parser true "use_thy" "use theory file"
     (name >> IsarCmd.use_thy);
 
-val loadP =
-  OuterSyntax.parser true "load" "load theory file"
-    (name >> IsarCmd.load);
+val update_thyP =
+  OuterSyntax.parser true "update_thy" "update theory file"
+    (name >> IsarCmd.use_thy);
 
 val prP =
   OuterSyntax.parser true "pr" "print current toplevel state"
@@ -532,13 +532,13 @@
   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
   print_thmsP, print_propP, print_termP, print_typeP,
   (*system commands*)
-  cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, restartP, breakP];
+  cdP, pwdP, use_thyP, update_thyP, prP, commitP, quitP, exitP,
+  restartP, breakP];
 
 
 end;
 
 
-(* install the Pure outer syntax *)
-
+(*install the Pure outer syntax*)
 OuterSyntax.add_keywords IsarSyn.keywords;
 OuterSyntax.add_parsers IsarSyn.parsers;