1.1 --- a/src/Pure/Thy/thy_output.ML	Tue Jun 24 19:43:19 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Jun 24 19:43:20 2008 +0200
     1.3 @@ -153,11 +153,13 @@
     1.4              options opts (fn () => command src node) ();  (*preview errors!*)
     1.5              PrintMode.with_modes (! modes @ Latex.modes)
     1.6                (Output.no_warnings (options opts (fn () => command src node))) ()
     1.7 -          end;
     1.8 +          end
     1.9 +      | expand (Antiquote.Open _) = ""
    1.10 +      | expand (Antiquote.Close _) = "";
    1.11      val ants = Antiquote.scan_antiquotes (str, pos);
    1.12    in
    1.13      if is_none node andalso exists Antiquote.is_antiq ants then
    1.14 -      error ("Cannot expand text antiquotations at top-level" ^ Position.str_of pos)
    1.15 +      error ("Unknown context -- cannot expand text antiquotations" ^ Position.str_of pos)
    1.16      else implode (map expand ants)
    1.17    end;
    1.18