src/Pure/Tools/update_header.scala
changeset 59083 88b0b1f28adc
parent 58872 f0f623005324
child 61463 8e46cea6a45a
--- 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) {