src/Pure/Thy/thy_header.scala

--- a/src/Pure/Thy/thy_header.scala	Tue Feb 26 20:11:11 2013 +0100
+++ b/src/Pure/Thy/thy_header.scala	Wed Feb 27 12:45:19 2013 +0100
@@ -22,12 +22,11 @@
   val IMPORTS = "imports"
   val KEYWORDS = "keywords"
   val AND = "and"
-  val USES = "uses"
   val BEGIN = "begin"
 
   private val lexicon =
     Scan.Lexicon("%", "(", ")", ",", "::", ";", "==",
-      AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
+      AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY)
 
 
   /* theory file name */
@@ -72,9 +71,8 @@
       theory_name ~
       (opt(keyword(IMPORTS) ~! (rep1(theory_name))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
       (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
-      (opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
       keyword(BEGIN) ^^
-      { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
+      { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs, Nil) }
 
     (keyword(HEADER) ~ tags) ~!
       ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
@@ -120,9 +118,9 @@
   name: String,
   imports: List[String],
   keywords: Thy_Header.Keywords,
-  uses: List[(String, Boolean)])
+  files: List[String])
 {
   def map(f: String => String): Thy_Header =
-    Thy_Header(f(name), imports.map(f), keywords, uses.map(p => (f(p._1), p._2)))
+    Thy_Header(f(name), imports.map(f), keywords, files.map(f))
 }