src/Pure/Thy/thy_output.ML
changeset 30613 b22d35d9ef28
parent 30590 1d9c9fcf8513
child 30635 a7d175c48228
--- a/src/Pure/Thy/thy_output.ML	Fri Mar 20 20:20:09 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Fri Mar 20 20:21:38 2009 +0100
@@ -156,7 +156,7 @@
           end
       | expand (Antiquote.Open _) = ""
       | expand (Antiquote.Close _) = "";
-    val ants = Antiquote.read Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
+    val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
   in
     if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
       error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)