# HG changeset patch # User wenzelm # Date 940370976 -7200 # Node ID 757dac39c5793a1a0713bdbad3259ec6526a163a # Parent 2c65e8212115592eb2684c155d43485d5a5845d8 fixed update_thy_only; diff -r 2c65e8212115 -r 757dac39c579 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Oct 19 16:23:46 1999 +0200 +++ b/src/Pure/Isar/isar_syn.ML Wed Oct 20 00:09:36 1999 +0200 @@ -540,7 +540,7 @@ val update_thy_onlyP = OuterSyntax.improper_command "update_thy_only" "update theory file, ignoring associated ML" - K.diag (P.name >> IsarCmd.update_thy); + K.diag (P.name >> IsarCmd.update_thy_only); val touch_thyP = OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag