| changeset 36948 | d2cdad45fd14 |
| parent 34300 | 3f2e25dc99ab |
| child 36956 | 21be4832c362 |
--- a/src/Pure/Thy/thy_header.scala Sat May 15 22:05:49 2010 +0200 +++ b/src/Pure/Thy/thy_header.scala Sat May 15 22:15:57 2010 +0200 @@ -27,7 +27,7 @@ } -class Thy_Header(symbols: Symbol.Interpretation) extends Outer_Parse.Parser +class Thy_Header(symbols: Symbol.Interpretation) extends Parse.Parser { import Thy_Header._