changeset 64854 | f5aa712e6250 |
parent 64825 | e78b62c289bb |
child 65362 | 908a27a4b9c9 |
--- a/src/Pure/Thy/thy_header.scala Mon Jan 09 19:34:16 2017 +0100 +++ b/src/Pure/Thy/thy_header.scala Mon Jan 09 20:26:59 2017 +0100 @@ -37,7 +37,7 @@ val AND = "and" val BEGIN = "begin" - private val bootstrap_header: Keywords = + val bootstrap_header: Keywords = List( ("%", Keyword.no_spec), ("(", Keyword.no_spec),