src/Pure/General/symbol_pos.ML
changeset 61707 d5ddd022a451
parent 61705 546e6494049f
child 62210 e068ea693678
     1.1 --- a/src/Pure/General/symbol_pos.ML	Thu Nov 19 22:21:51 2015 +0100
     1.2 +++ b/src/Pure/General/symbol_pos.ML	Thu Nov 19 22:35:10 2015 +0100
     1.3 @@ -74,9 +74,7 @@
     1.4            | (line, nl :: rest) => line :: split rest);
     1.5        in split list end;
     1.6  
     1.7 -val trim_blanks =
     1.8 -  take_prefix (Symbol.is_blank o symbol) #> #2 #>
     1.9 -  take_suffix (Symbol.is_blank o symbol) #> #1;
    1.10 +val trim_blanks = trim (Symbol.is_blank o symbol);
    1.11  
    1.12  val trim_lines =
    1.13    split_lines #> map trim_blanks #> separate [(Symbol.space, Position.none)] #> flat;