| changeset 24577 | c6acb6d79757 |
| parent 23863 | 8f3099589cfa |
| child 24739 | e9f9d4297bda |
--- a/src/Pure/Thy/thy_header.ML Fri Sep 14 22:22:53 2007 +0200 +++ b/src/Pure/Thy/thy_header.ML Sat Sep 15 19:25:19 2007 +0200 @@ -27,8 +27,8 @@ val usesN = "uses"; val beginN = "begin"; -val header_lexicon = T.make_lexicon - ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN]; +val header_lexicon = Scan.make_lexicon + (map Symbol.explode ["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN]); (* header args *)