diff -r 25501ba956ac -r 88b0b1f28adc src/Pure/Tools/update_header.scala --- a/src/Pure/Tools/update_header.scala Wed Dec 03 11:50:58 2014 +0100 +++ b/src/Pure/Tools/update_header.scala Wed Dec 03 14:04:38 2014 +0100 @@ -13,7 +13,7 @@ { val text0 = File.read(path) val text1 = - (for (tok <- Outer_Syntax.empty.scan(text0).iterator) + (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator) yield { if (tok.source == "header") section else tok.source }).mkString if (text0 != text1) {