tuned;
authorwenzelm
Sat, 30 May 2009 11:56:21 +0200
changeset 31297 a176e4dfb388
parent 31296 ba296a58d813
child 31298 5e6b2b23701a
tuned;
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