diff --git a/src/Pure/Thy/latex.ML b/src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML
+++ b/src/Pure/Thy/latex.ML
@@ -1,279 +1,276 @@
 (*  Title:      Pure/Thy/latex.ML
     Author:     Makarius
 
 LaTeX output of theory sources.
 *)
 
 signature LATEX =
 sig
   type text = XML.body
   val text: string * Position.T -> text
   val string: string -> text
   val block: text -> XML.tree
   val enclose_text: string -> string -> text -> text
   val output_text: text -> string
   val output_name: string -> string
   val output_ascii: string -> string
   val output_ascii_breakable: string -> string -> string
   val output_symbols: Symbol.symbol list -> string
   val output_syms: string -> string
   val symbols: Symbol_Pos.T list -> text
   val symbols_output: Symbol_Pos.T list -> text
   val begin_delim: string -> string
   val end_delim: string -> string
   val begin_tag: string -> string
   val end_tag: string -> string
   val environment_text: string -> text -> text
-  val environment: string -> string -> string
   val isabelle_body: string -> text -> text
   val theory_entry: string -> string
   val index_escape: string -> string
   type index_item = {text: text, like: string}
   type index_entry = {items: index_item list, def: bool}
   val index_entry: index_entry -> text
   val index_variants: (binding -> bool option -> 'a -> 'a) -> binding -> 'a -> 'a
   val latexN: string
   val latex_output: string -> string * int
   val latex_markup: string * Properties.T -> Markup.output
   val latex_indent: string -> int -> string
 end;
 
 structure Latex: LATEX =
 struct
 
 (* text with positions *)
 
 type text = XML.body;
 
 fun text (s, pos) =
   if s = "" then []
   else if pos = Position.none then [XML.Text s]
   else [XML.Elem (Position.markup pos Markup.document_latex, [XML.Text s])];
 
 fun string s = text (s, Position.none);
 
 fun block body = XML.Elem (Markup.document_latex, body);
 
 val output_text =
   let
     fun document_latex text =
       text |> maps
         (fn XML.Elem ((name, _), body) =>
               if name = Markup.document_latexN then document_latex body else []
           | t => [t])
   in XML.content_of o document_latex end;
 
 fun enclose_text bg en body = string bg @ body @ string en;
 
 
 (* output name for LaTeX macros *)
 
 val output_name =
   translate_string
     (fn "_" => "UNDERSCORE"
       | "'" => "PRIME"
       | "0" => "ZERO"
       | "1" => "ONE"
       | "2" => "TWO"
       | "3" => "THREE"
       | "4" => "FOUR"
       | "5" => "FIVE"
       | "6" => "SIX"
       | "7" => "SEVEN"
       | "8" => "EIGHT"
       | "9" => "NINE"
       | s => s);
 
 fun enclose_name bg en = enclose bg en o output_name;
 
 
 (* output verbatim ASCII *)
 
 val output_ascii =
   translate_string
     (fn " " => "\\ "
       | "\t" => "\\ "
       | "\n" => "\\isanewline\n"
       | s =>
           s
           |> exists_string (fn s' => s = s') "\"#$%&',-<>\\^_`{}~" ? enclose "{\\char`\\" "}"
           |> suffix "{\\kern0pt}");
 
 fun output_ascii_breakable sep =
   space_explode sep
   #> map output_ascii
   #> space_implode (output_ascii sep ^ "\\discretionary{}{}{}");
 
 
 (* output symbols *)
 
 local
 
 val char_table =
   Symtab.make
    [("\007", "{\\isacharbell}"),
     ("!", "{\\isacharbang}"),
     ("\"", "{\\isachardoublequote}"),
     ("#", "{\\isacharhash}"),
     ("$", "{\\isachardollar}"),
     ("%", "{\\isacharpercent}"),
     ("&", "{\\isacharampersand}"),
     ("'", "{\\isacharprime}"),
     ("(", "{\\isacharparenleft}"),
     (")", "{\\isacharparenright}"),
     ("*", "{\\isacharasterisk}"),
     ("+", "{\\isacharplus}"),
     (",", "{\\isacharcomma}"),
     ("-", "{\\isacharminus}"),
     (".", "{\\isachardot}"),
     ("/", "{\\isacharslash}"),
     (":", "{\\isacharcolon}"),
     (";", "{\\isacharsemicolon}"),
     ("<", "{\\isacharless}"),
     ("=", "{\\isacharequal}"),
     (">", "{\\isachargreater}"),
     ("?", "{\\isacharquery}"),
     ("@", "{\\isacharat}"),
     ("[", "{\\isacharbrackleft}"),
     ("\\", "{\\isacharbackslash}"),
     ("]", "{\\isacharbrackright}"),
     ("^", "{\\isacharcircum}"),
     ("_", "{\\isacharunderscore}"),
     ("`", "{\\isacharbackquote}"),
     ("{", "{\\isacharbraceleft}"),
     ("|", "{\\isacharbar}"),
     ("}", "{\\isacharbraceright}"),
     ("~", "{\\isachartilde}")];
 
 fun output_chr " " = "\\ "
   | output_chr "\t" = "\\ "
   | output_chr "\n" = "\\isanewline\n"
   | output_chr c =
       (case Symtab.lookup char_table c of
         SOME s => s ^ "{\\kern0pt}"
       | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
 
 fun output_sym sym =
   (case Symbol.decode sym of
     Symbol.Char s => output_chr s
   | Symbol.UTF8 s => s
   | Symbol.Sym s => enclose_name "{\\isasym" "}" s
   | Symbol.Control s => enclose_name "\\isactrl" " " s
   | Symbol.Malformed s => error (Symbol.malformed_msg s)
   | Symbol.EOF => error "Bad EOF symbol");
 
 open Basic_Symbol_Pos;
 
 val scan_latex_length =
   Scan.many1 (fn (s, _) => s <> Symbol.latex andalso Symbol.not_eof s)
     >> (Symbol.length o map Symbol_Pos.symbol) ||
   $$ Symbol.latex -- Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0;
 
 val scan_latex =
   $$ Symbol.latex |-- Symbol_Pos.scan_cartouche_content "Embedded LaTeX: "
     >> (implode o map Symbol_Pos.symbol) ||
   Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_sym o Symbol_Pos.symbol);
 
 fun read scan syms =
   Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms);
 
 in
 
 fun length_symbols syms =
   fold Integer.add (these (read scan_latex_length syms)) 0;
 
 fun output_symbols syms =
   if member (op =) syms Symbol.latex then
     (case read scan_latex syms of
       SOME ss => implode ss
     | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)))
   else implode (map output_sym syms);
 
 val output_syms = output_symbols o Symbol.explode;
 
 end;
 
 fun symbols syms = text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms));
 fun symbols_output syms =
   text (output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms));
 
 
 (* tags *)
 
 val begin_delim = enclose_name "%\n\\isadelim" "\n";
 val end_delim = enclose_name "%\n\\endisadelim" "\n";
 val begin_tag = enclose_name "%\n\\isatag" "\n";
 fun end_tag tg = enclose_name "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
 
 
 (* theory presentation *)
 
-fun environment_delim name =
- ("%\n\\begin{" ^ output_name name ^ "}%\n",
-  "%\n\\end{" ^ output_name name ^ "}");
-
-fun environment_text name = environment_delim name |-> enclose_text;
-fun environment name = environment_delim name |-> enclose;
+fun environment_text name =
+  enclose_text
+    ("%\n\\begin{" ^ output_name name ^ "}%\n")
+    ("%\n\\end{" ^ output_name name ^ "}");
 
 fun isabelle_body name =
   enclose_text
    ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n")
    "%\n\\end{isabellebody}%\n";
 
 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
 
 
 (* index entries *)
 
 type index_item = {text: text, like: string};
 type index_entry = {items: index_item list, def: bool};
 
 val index_escape =
   translate_string (fn s =>
     if member_string "!\"@|" s then "\\char" ^ string_of_int (ord s)
     else if member_string "\\{}#" s then "\"" ^ s else s);
 
 fun index_item (item: index_item) =
   let
     val like_text =
       if #like item = "" then ""
       else index_escape (#like item) ^ "@";
     val item_text = index_escape (output_text (#text item));
   in like_text ^ item_text end;
 
 fun index_entry (entry: index_entry) =
   (space_implode "!" (map index_item (#items entry)) ^
     "|" ^ index_escape (if #def entry then "isaindexdef" else "isaindexref"))
   |> enclose "\\index{" "}"
   |> string;
 
 fun index_binding NONE = I
   | index_binding (SOME def) = Binding.map_name (suffix (if def then "_def" else "_ref"));
 
 fun index_variants setup binding =
   fold (fn index => setup (index_binding index binding) index) [NONE, SOME true, SOME false];
 
 
 (* print mode *)
 
 val latexN = "latex";
 
 fun latex_output str =
   let val syms = Symbol.explode str
   in (output_symbols syms, length_symbols syms) end;
 
 fun latex_markup (s, _: Properties.T) =
   if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N
   then ("\\isacommand{", "}")
   else if s = Markup.keyword2N
   then ("\\isakeyword{", "}")
   else Markup.no_output;
 
 fun latex_indent "" _ = ""
   | latex_indent s _ = enclose "\\isaindent{" "}" s;
 
 val _ = Output.add_mode latexN latex_output (prefix Symbol.latex o cartouche);
 val _ = Markup.add_mode latexN latex_markup;
 val _ = Pretty.add_mode latexN latex_indent;
 
 end;
diff --git a/src/Pure/Tools/rail.ML b/src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML
+++ b/src/Pure/Tools/rail.ML
@@ -1,392 +1,392 @@
 (*  Title:      Pure/Tools/rail.ML
     Author:     Michael Kerscher, TU München
     Author:     Makarius
 
 Railroad diagrams in LaTeX.
 *)
 
 signature RAIL =
 sig
   datatype rails =
     Cat of int * rail list
   and rail =
     Bar of rails list |
     Plus of rails * rails |
     Newline of int |
     Nonterminal of string |
     Terminal of bool * string |
     Antiquote of bool * Antiquote.antiq
   val read: Proof.context -> Input.source -> (string Antiquote.antiquote * rail) list
   val output_rules: Proof.context -> (string Antiquote.antiquote * rail) list -> Latex.text
 end;
 
 structure Rail: RAIL =
 struct
 
 (** lexical syntax **)
 
 (* singleton keywords *)
 
 val keywords =
   Symtab.make [
     ("|", Markup.keyword3),
     ("*", Markup.keyword3),
     ("+", Markup.keyword3),
     ("?", Markup.keyword3),
     ("(", Markup.empty),
     (")", Markup.empty),
     ("\<newline>", Markup.keyword2),
     (";", Markup.keyword2),
     (":", Markup.keyword2),
     ("@", Markup.keyword1)];
 
 
 (* datatype token *)
 
 datatype kind =
   Keyword | Ident | String | Space | Comment of Comment.kind | Antiq of Antiquote.antiq | EOF;
 
 datatype token = Token of Position.range * (kind * string);
 
 fun pos_of (Token ((pos, _), _)) = pos;
 fun end_pos_of (Token ((_, pos), _)) = pos;
 
 fun range_of (toks as tok :: _) =
       let val pos' = end_pos_of (List.last toks)
       in Position.range (pos_of tok, pos') end
   | range_of [] = Position.no_range;
 
 fun kind_of (Token (_, (k, _))) = k;
 fun content_of (Token (_, (_, x))) = x;
 
 fun is_proper (Token (_, (Space, _))) = false
   | is_proper (Token (_, (Comment _, _))) = false
   | is_proper _ = true;
 
 
 (* diagnostics *)
 
 val print_kind =
  fn Keyword => "rail keyword"
   | Ident => "identifier"
   | String => "single-quoted string"
   | Space => "white space"
   | Comment _ => "formal comment"
   | Antiq _ => "antiquotation"
   | EOF => "end-of-input";
 
 fun print (Token ((pos, _), (k, x))) =
   (if k = EOF then print_kind k else print_kind k ^ " " ^ quote x) ^
   Position.here pos;
 
 fun print_keyword x = print_kind Keyword ^ " " ^ quote x;
 
 fun reports_of_token (Token ((pos, _), (Keyword, x))) =
       map (pair pos) (the_list (Symtab.lookup keywords x) @ Completion.suppress_abbrevs x)
   | reports_of_token (Token ((pos, _), (String, _))) = [(pos, Markup.inner_string)]
   | reports_of_token (Token (_, (Antiq antiq, _))) = Antiquote.antiq_reports [Antiquote.Antiq antiq]
   | reports_of_token _ = [];
 
 
 (* stopper *)
 
 fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
 val eof = mk_eof Position.none;
 
 fun is_eof (Token (_, (EOF, _))) = true
   | is_eof _ = false;
 
 val stopper =
   Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
 
 
 (* tokenize *)
 
 local
 
 fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))];
 
 fun antiq_token antiq =
   [Token (#range antiq, (Antiq antiq, Symbol_Pos.content (#body antiq)))];
 
 val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);
 
 val scan_keyword =
   Scan.one (Symtab.defined keywords o Symbol_Pos.symbol);
 
 val err_prefix = "Rail lexical error: ";
 
 val scan_token =
   scan_space >> token Space ||
   Comment.scan_inner >> (fn (kind, ss) => token (Comment kind) ss) ||
   Antiquote.scan_antiq >> antiq_token ||
   scan_keyword >> (token Keyword o single) ||
   Lexicon.scan_id >> token Ident ||
   Symbol_Pos.scan_string_q err_prefix >> (fn (pos1, (ss, pos2)) =>
     [Token (Position.range (pos1, pos2), (String, Symbol_Pos.content ss))]);
 
 val scan =
   Scan.repeats scan_token --|
     Symbol_Pos.!!! (fn () => err_prefix ^ "bad input")
       (Scan.ahead (Scan.one Symbol_Pos.is_eof));
 
 in
 
 val tokenize = #1 o Scan.error (Scan.finite Symbol_Pos.stopper scan);
 
 end;
 
 
 
 (** parsing **)
 
 (* parser combinators *)
 
 fun !!! scan =
   let
     val prefix = "Rail syntax error";
 
     fun get_pos [] = " (end-of-input)"
       | get_pos (tok :: _) = Position.here (pos_of tok);
 
     fun err (toks, NONE) = (fn () => prefix ^ get_pos toks)
       | err (toks, SOME msg) =
           (fn () =>
             let val s = msg () in
               if String.isPrefix prefix s then s
               else prefix ^ get_pos toks ^ ": " ^ s
             end);
   in Scan.!! err scan end;
 
 fun $$$ x =
   Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) ||
   Scan.fail_with
     (fn [] => (fn () => print_keyword x ^ " expected,\nbut end-of-input was found")
       | tok :: _ => (fn () => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found"));
 
 fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
 fun enum sep scan = enum1 sep scan || Scan.succeed [];
 
 val ident = Scan.some (fn tok => if kind_of tok = Ident then SOME (content_of tok) else NONE);
 val string = Scan.some (fn tok => if kind_of tok = String then SOME (content_of tok) else NONE);
 
 val antiq = Scan.some (fn tok => (case kind_of tok of Antiq a => SOME a | _ => NONE));
 
 fun RANGE scan = Scan.trace scan >> apsnd range_of;
 fun RANGE_APP scan = RANGE scan >> (fn (f, r) => f r);
 
 
 (* parse trees *)
 
 datatype trees =
   CAT of tree list * Position.range
 and tree =
   BAR of trees list * Position.range |
   STAR of (trees * trees) * Position.range |
   PLUS of (trees * trees) * Position.range |
   MAYBE of tree * Position.range |
   NEWLINE of Position.range |
   NONTERMINAL of string * Position.range |
   TERMINAL of (bool * string) * Position.range |
   ANTIQUOTE of (bool * Antiquote.antiq) * Position.range;
 
 fun reports_of_tree ctxt =
   if Context_Position.reports_enabled ctxt then
     let
       fun reports r =
         if r = Position.no_range then []
         else [(Position.range_position r, Markup.expression "")];
       fun trees (CAT (ts, r)) = reports r @ maps tree ts
       and tree (BAR (Ts, r)) = reports r @ maps trees Ts
         | tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2
         | tree (PLUS ((T1, T2), r)) = reports r @ trees T1 @ trees T2
         | tree (MAYBE (t, r)) = reports r @ tree t
         | tree (NEWLINE r) = reports r
         | tree (NONTERMINAL (_, r)) = reports r
         | tree (TERMINAL (_, r)) = reports r
         | tree (ANTIQUOTE (_, r)) = reports r;
     in distinct (op =) o tree end
   else K [];
 
 local
 
 val at_mode = Scan.option ($$$ "@") >> (fn NONE => false | _ => true);
 
 fun body x = (RANGE (enum1 "|" body1) >> BAR) x
 and body0 x = (RANGE (enum "|" body1) >> BAR) x
 and body1 x =
  (RANGE_APP (body2 :|-- (fn a =>
    $$$ "*" |-- !!! body4e >> (fn b => fn r => CAT ([STAR ((a, b), r)], r)) ||
    $$$ "+" |-- !!! body4e >> (fn b => fn r => CAT ([PLUS ((a, b), r)], r)) ||
    Scan.succeed (K a)))) x
 and body2 x = (RANGE (Scan.repeat1 body3) >> CAT) x
 and body3 x =
  (RANGE_APP (body4 :|-- (fn a =>
    $$$ "?" >> K (curry MAYBE a) ||
    Scan.succeed (K a)))) x
 and body4 x =
  ($$$ "(" |-- !!! (body0 --| $$$ ")") ||
   RANGE_APP
    ($$$ "\<newline>" >> K NEWLINE ||
     ident >> curry NONTERMINAL ||
     at_mode -- string >> curry TERMINAL ||
     at_mode -- antiq >> curry ANTIQUOTE)) x
 and body4e x =
   (RANGE (Scan.option body4) >> (fn (a, r) => CAT (the_list a, r))) x;
 
 val rule_name = ident >> Antiquote.Text || antiq >> Antiquote.Antiq;
 val rule = rule_name -- ($$$ ":" |-- !!! body) || body >> pair (Antiquote.Text "");
 val rules = enum1 ";" (Scan.option rule) >> map_filter I;
 
 in
 
 fun parse_rules toks =
   #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks);
 
 end;
 
 
 (** rail expressions **)
 
 (* datatype *)
 
 datatype rails =
   Cat of int * rail list
 and rail =
   Bar of rails list |
   Plus of rails * rails |
   Newline of int |
   Nonterminal of string |
   Terminal of bool * string |
   Antiquote of bool * Antiquote.antiq;
 
 fun is_newline (Newline _) = true | is_newline _ = false;
 
 
 (* prepare *)
 
 local
 
 fun cat rails = Cat (0, rails);
 
 val empty = cat [];
 fun is_empty (Cat (_, [])) = true | is_empty _ = false;
 
 fun bar [Cat (_, [rail])] = rail
   | bar cats = Bar cats;
 
 fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
 and reverse (Bar cats) = Bar (map reverse_cat cats)
   | reverse (Plus (cat1, cat2)) = Plus (reverse_cat cat1, reverse_cat cat2)
   | reverse x = x;
 
 fun plus (cat1, cat2) = Plus (cat1, reverse_cat cat2);
 
 in
 
 fun prepare_trees (CAT (ts, _)) = Cat (0, map prepare_tree ts)
 and prepare_tree (BAR (Ts, _)) = bar (map prepare_trees Ts)
   | prepare_tree (STAR (Ts, _)) =
       let val (cat1, cat2) = apply2 prepare_trees Ts in
         if is_empty cat2 then plus (empty, cat1)
         else bar [empty, cat [plus (cat1, cat2)]]
       end
   | prepare_tree (PLUS (Ts, _)) = plus (apply2 prepare_trees Ts)
   | prepare_tree (MAYBE (t, _)) = bar [empty, cat [prepare_tree t]]
   | prepare_tree (NEWLINE _) = Newline 0
   | prepare_tree (NONTERMINAL (a, _)) = Nonterminal a
   | prepare_tree (TERMINAL (a, _)) = Terminal a
   | prepare_tree (ANTIQUOTE (a, _)) = Antiquote a;
 
 end;
 
 
 (* read *)
 
 fun read ctxt source =
   let
     val _ = Context_Position.report ctxt (Input.pos_of source) Markup.language_rail;
     val toks = tokenize (Input.source_explode source);
     val _ = Context_Position.reports ctxt (maps reports_of_token toks);
     val rules = parse_rules (filter is_proper toks);
     val _ = Context_Position.reports ctxt (maps (reports_of_tree ctxt o #2) rules);
   in map (apsnd prepare_tree) rules end;
 
 
 (* latex output *)
 
 local
 
 fun vertical_range_cat (Cat (_, rails)) y =
   let val (rails', (_, y')) =
     fold_map (fn rail => fn (y0, y') =>
       if is_newline rail then (Newline (y' + 1), (y' + 1, y' + 2))
       else
         let val (rail', y0') = vertical_range rail y0;
         in (rail', (y0, Int.max (y0', y'))) end) rails (y, y + 1)
   in (Cat (y, rails'), y') end
 
 and vertical_range (Bar cats) y =
       let val (cats', y') = fold_map vertical_range_cat cats y
       in (Bar cats', Int.max (y + 1, y')) end
   | vertical_range (Plus (cat1, cat2)) y =
       let val ([cat1', cat2'], y') = fold_map vertical_range_cat [cat1, cat2] y;
       in (Plus (cat1', cat2'), Int.max (y + 1, y')) end
   | vertical_range (Newline _) y = (Newline (y + 2), y + 3)
   | vertical_range atom y = (atom, y + 1);
 
 in
 
 fun output_rules ctxt rules =
   let
     val output_antiq =
       Antiquote.Antiq #>
       Document_Antiquotation.evaluate Latex.symbols ctxt #>
       Latex.output_text;
     fun output_text b s =
       Output.output s
       |> b ? enclose "\\isakeyword{" "}"
       |> enclose "\\isa{" "}";
 
     fun output_cat c (Cat (_, rails)) = outputs c rails
     and outputs c [rail] = output c rail
       | outputs _ rails = implode (map (output "") rails)
     and output _ (Bar []) = ""
       | output c (Bar [cat]) = output_cat c cat
       | output _ (Bar (cat :: cats)) =
           "\\rail@bar\n" ^ output_cat "" cat ^
           implode (map (fn Cat (y, rails) =>
               "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^
           "\\rail@endbar\n"
       | output c (Plus (cat, Cat (y, rails))) =
           "\\rail@plus\n" ^ output_cat c cat ^
           "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^
           "\\rail@endplus\n"
       | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n"
       | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text false s ^ "}[]\n"
       | output c (Terminal (b, s)) = "\\rail@" ^ c ^ "term{" ^ output_text b s ^ "}[]\n"
       | output c (Antiquote (b, a)) =
           "\\rail@" ^ c ^ (if b then "term{" else "nont{") ^ output_antiq a ^ "}[]\n";
 
     fun output_rule (name, rail) =
       let
         val (rail', y') = vertical_range rail 0;
         val out_name =
           (case name of
             Antiquote.Text "" => ""
           | Antiquote.Text s => output_text false s
           | Antiquote.Antiq a => output_antiq a);
       in
         "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ out_name ^ "}\n" ^
         output "" rail' ^
         "\\rail@end\n"
       end;
-  in Latex.string (Latex.environment "railoutput" (implode (map output_rule rules))) end;
+  in Latex.environment_text "railoutput" (Latex.string (implode (map output_rule rules))) end;
 
 val _ = Theory.setup
   (Document_Output.antiquotation_raw_embedded \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
     (fn ctxt => output_rules ctxt o read ctxt));
 
 end;
 
 end;