# HG changeset patch
# User wenzelm
# Date 1243677381 -7200
# Node ID a176e4dfb388003e0dcd3ae6fa513b2fe65edcae
# Parent  ba296a58d81354ac4a67c131d06a5286c94b0d9c
tuned;

diff -r ba296a58d813 -r a176e4dfb388 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Sat May 30 08:17:05 2009 +0200
+++ b/doc-src/antiquote_setup.ML	Sat May 30 11:56:21 2009 +0200
@@ -159,9 +159,9 @@
       end);
 
 fun entity_antiqs check markup kind =
- [(entity check markup kind NONE),
-  (entity check markup kind (SOME true)),
-  (entity check markup kind (SOME false))];
+ ((entity check markup kind NONE);
+  (entity check markup kind (SOME true));
+  (entity check markup kind (SOME false)));
 
 in