# HG changeset patch
# User wenzelm
# Date 918057006 -3600
# Node ID 4328d436c556bfee8582ee0d34300da57eb9cc9a
# Parent  f9fdb4e297903cda82897478c4b3a70f021def94
oops, update_thy;

diff -r f9fdb4e29790 -r 4328d436c556 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Feb 03 16:49:36 1999 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Feb 03 16:50:06 1999 +0100
@@ -469,7 +469,7 @@
 
 val update_thyP =
   OuterSyntax.parser true "update_thy" "update theory file"
-    (name >> IsarCmd.use_thy);
+    (name >> IsarCmd.update_thy);
 
 val prP =
   OuterSyntax.parser true "pr" "print current toplevel state"