--- a/CookBook/Recipes/Antiquotes.thy	Fri Feb 27 15:59:38 2009 +0000
+++ b/CookBook/Recipes/Antiquotes.thy	Sat Feb 28 14:18:02 2009 +0000
@@ -16,6 +16,9 @@
   various entities in a document. They can also be used for sophisticated
   \LaTeX-hacking. If you type @{text "Ctrl-c Ctrl-a h A"} inside ProofGeneral, you
   obtain a list of all currently available document antiquotations and their options.
+  You obtain the same list on the ML-level by typing
+
+  @{ML [display,gray] "ThyOutput.print_antiquotations ()"}
 
   Below we give the code for two additional antiquotations that can be used to typeset
   ML-code and also to check whether the given code actually compiles. This