src/Pure/Tools/rail.ML
changeset 62806 de9bf8171626
parent 62797 e08c44eed27f
child 67147 dea94b1aabc3
     1.1 --- a/src/Pure/Tools/rail.ML	Fri Apr 01 19:01:34 2016 +0200
     1.2 +++ b/src/Pure/Tools/rail.ML	Fri Apr 01 21:34:17 2016 +0200
     1.3 @@ -188,7 +188,7 @@
     1.4      let
     1.5        fun reports r =
     1.6          if r = Position.no_range then []
     1.7 -        else [(Position.range_position r, Markup.expression)];
     1.8 +        else [(Position.range_position r, Markup.expression "")];
     1.9        fun trees (CAT (ts, r)) = reports r @ maps tree ts
    1.10        and tree (BAR (Ts, r)) = reports r @ maps trees Ts
    1.11          | tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2