src/Pure/Thy/thy_output.ML
changeset 30642 0c9f9c49d5df
parent 30635 a7d175c48228
child 30683 e8ac1f9d9469
     1.1 --- a/src/Pure/Thy/thy_output.ML	Sun Mar 22 20:49:47 2009 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Mar 22 20:49:47 2009 +0100
     1.3 @@ -156,7 +156,7 @@
     1.4            end
     1.5        | expand (Antiquote.Open _) = ""
     1.6        | expand (Antiquote.Close _) = "";
     1.7 -    val ants = Antiquote.read (K ()) Antiquote.scan_text (Symbol_Pos.explode (txt, pos), pos);
     1.8 +    val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
     1.9    in
    1.10      if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then
    1.11        error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)