author | wenzelm |
Wed, 22 Aug 2012 21:43:17 +0200 | |
changeset 48889 | 04deeb14327c |
parent 48888 | 74ad16f79425 |
child 48890 | d72ca5742f80 |
--- a/src/Pure/Thy/thy_load.scala Wed Aug 22 21:28:33 2012 +0200 +++ b/src/Pure/Thy/thy_load.scala Wed Aug 22 21:43:17 2012 +0200 @@ -108,7 +108,7 @@ { val string = text.toString val header = check_thy_text(name, string) - val more_uses = find_files(syntax, string) + val more_uses = find_files(syntax.add_keywords(header.keywords), string) header.copy(uses = header.uses ::: more_uses.map((_, false))) }) }