src/Pure/Thy/thy_header.ML

--- a/src/Pure/Thy/thy_header.ML	Wed Feb 27 12:45:19 2013 +0100
+++ b/src/Pure/Thy/thy_header.ML	Wed Feb 27 16:27:44 2013 +0100
@@ -10,9 +10,8 @@
   type header =
    {name: string * Position.T,
     imports: (string * Position.T) list,
-    keywords: keywords,
-    files: Path.T list}
-  val make: string * Position.T -> (string * Position.T) list -> keywords -> Path.T list -> header
+    keywords: keywords}
+  val make: string * Position.T -> (string * Position.T) list -> keywords -> header
   val define_keywords: header -> unit
   val declare_keyword: string * Keyword.spec option -> theory -> theory
   val the_keyword: theory -> string -> Keyword.spec option
@@ -29,11 +28,10 @@
 type header =
  {name: string * Position.T,
   imports: (string * Position.T) list,
-  keywords: keywords,
-  files: Path.T list};
+  keywords: keywords};
 
-fun make name imports keywords files : header =
-  {name = name, imports = imports, keywords = keywords, files = files};
+fun make name imports keywords : header =
+  {name = name, imports = imports, keywords = keywords};
 
 
 
@@ -111,7 +109,7 @@
   Scan.optional (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) [] --
   Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
   Parse.$$$ beginN >>
-  (fn ((name, imports), keywords) => make name imports keywords []);
+  (fn ((name, imports), keywords) => make name imports keywords);
 
 end;