# HG changeset patch
# User wenzelm
# Date 870861391 -7200
# Node ID ed1416badb41af00e16986a84929b1846c0f08ab
# Parent  0fc67ad6d62a51354d018c7cd589f98c99de9079
oops;

diff -r 0fc67ad6d62a -r ed1416badb41 src/Pure/Thy/thy_syn.ML
--- a/src/Pure/Thy/thy_syn.ML	Wed Aug 06 11:52:16 1997 +0200
+++ b/src/Pure/Thy/thy_syn.ML	Wed Aug 06 11:56:31 1997 +0200
@@ -30,7 +30,7 @@
 (* augment syntax *)
 
 fun add_syntax keys sects =
- (keywords := keys union ! keywords;
+ (keywords := (keys union ! keywords);
   sections := sects @ ! sections;
   syntax := make_syntax ());