diff -r cb6421b6a18f -r b22d35d9ef28 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Fri Mar 20 20:20:09 2009 +0100
+++ b/src/Pure/General/antiquote.ML	Fri Mar 20 20:21:38 2009 +0100
@@ -14,7 +14,7 @@
   val is_antiq: 'a antiquote -> bool
   val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
   val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
-  val read: (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
+  val read: ('a -> unit) -> (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) ->
     Symbol_Pos.T list * Position.T -> 'a antiquote list
 end;
 
@@ -83,13 +83,12 @@
 
 (* read *)
 
-fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
-  | report_antiq _ = ();
-
-fun read _ ([], _) = []
-  | read scanner (syms, pos) =
+fun read _ _ ([], _) = []
+  | read report scanner (syms, pos) =
       (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of
-        SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
+        SOME xs =>
+         (List.app (fn Antiq (_, pos) => Position.report Markup.antiq pos | Text x => report x) xs;
+          check_nesting xs; xs)
       | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
 
 end;