diff -r f673ce6b1e2b -r 9830c944670f src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Fri Apr 03 18:36:19 2015 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Apr 03 19:56:51 2015 +0200
@@ -17,7 +17,7 @@
   val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
   val check_command: Proof.context -> xstring * Position.T -> string
   val check_option: Proof.context -> xstring * Position.T -> string
-  val print_antiquotations: Proof.context -> unit
+  val print_antiquotations: bool -> Proof.context -> unit
   val antiquotation: binding -> 'a context_parser ->
     ({source: Token.src, state: Toplevel.state, context: Proof.context} -> 'a -> string) ->
       theory -> theory
@@ -104,11 +104,11 @@
       Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos);
   in opt s ctxt end;
 
-fun print_antiquotations ctxt =
+fun print_antiquotations verbose ctxt =
   let
     val (commands, options) = get_antiquotations ctxt;
-    val command_names = map #1 (Name_Space.markup_table ctxt commands);
-    val option_names = map #1 (Name_Space.markup_table ctxt options);
+    val command_names = map #1 (Name_Space.markup_table verbose ctxt commands);
+    val option_names = map #1 (Name_Space.markup_table verbose ctxt options);
   in
     [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
      Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]