discontinued obsolete 'uses' within theory header;
authorwenzelm
Wed Feb 27 12:45:19 2013 +0100 (2013-02-27)
changeset 5129305b1bbae748d
parent 51287 8799eadf61fb
child 51294 0850d43cb355
discontinued obsolete 'uses' within theory header;
NEWS
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/HOL/Mirabelle/lib/scripts/mirabelle.pl
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Pure.thy
src/Pure/Thy/present.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_load.scala
src/Pure/Tools/build.scala
     1.1 --- a/NEWS	Tue Feb 26 20:11:11 2013 +0100
     1.2 +++ b/NEWS	Wed Feb 27 12:45:19 2013 +0100
     1.3 @@ -4,6 +4,13 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** General ***
     1.8 +
     1.9 +* Discontinued obsolete 'uses' within theory header.  Note that
    1.10 +commands like 'ML_file' work without separate declaration of file
    1.11 +dependencies.  Minor INCOMPATIBILITY.
    1.12 +
    1.13 +
    1.14  *** HOL ***
    1.15  
    1.16  * Discontinued obsolete src/HOL/IsaMakefile (considered legacy since
     2.1 --- a/etc/isar-keywords-ZF.el	Tue Feb 26 20:11:11 2013 +0100
     2.2 +++ b/etc/isar-keywords-ZF.el	Wed Feb 27 12:45:19 2013 +0100
     2.3 @@ -249,7 +249,6 @@
     2.4      "type_elims"
     2.5      "type_intros"
     2.6      "unchecked"
     2.7 -    "uses"
     2.8      "where"))
     2.9  
    2.10  (defconst isar-keywords-control
     3.1 --- a/etc/isar-keywords.el	Tue Feb 26 20:11:11 2013 +0100
     3.2 +++ b/etc/isar-keywords.el	Wed Feb 27 12:45:19 2013 +0100
     3.3 @@ -346,7 +346,6 @@
     3.4      "structure"
     3.5      "unchecked"
     3.6      "unsafe"
     3.7 -    "uses"
     3.8      "where"))
     3.9  
    3.10  (defconst isar-keywords-control
     4.1 --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Tue Feb 26 20:11:11 2013 +0100
     4.2 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Wed Feb 27 12:45:19 2013 +0100
     4.3 @@ -69,7 +69,7 @@
     4.4    my $s = join ("\n", @action_files);
     4.5    my @action_files = split(/\n/, $s . "\n" . $s);
     4.6    %action_files = sort(@action_files);
     4.7 -  $tools = "uses " . join(" ", sort(keys(%action_files)));
     4.8 +  $tools = join("", map { "ML_file " . $_ . "\n" } (sort(keys(%action_files))));
     4.9  }
    4.10  
    4.11  open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
    4.12 @@ -77,8 +77,9 @@
    4.13  print SETUP_FILE <<END;
    4.14  theory "$setup_thy_name"
    4.15  imports "$mirabelle_thy" "$mirabelle_theory"
    4.16 +begin
    4.17 +
    4.18  $tools
    4.19 -begin
    4.20  
    4.21  setup {*
    4.22    Config.put_global Mirabelle.logfile "$log_file" #>
     5.1 --- a/src/Pure/PIDE/document.ML	Tue Feb 26 20:11:11 2013 +0100
     5.2 +++ b/src/Pure/PIDE/document.ML	Wed Feb 27 12:45:19 2013 +0100
     5.3 @@ -102,9 +102,9 @@
     5.4  
     5.5  fun read_header node span =
     5.6    let
     5.7 -    val (dir, {name = (name, _), imports, keywords, uses}) = get_header node;
     5.8 +    val (dir, {name = (name, _), imports, keywords, files}) = get_header node;
     5.9      val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
    5.10 -  in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords uses) end;
    5.11 +  in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords files) end;
    5.12  
    5.13  fun get_perspective (Node {perspective, ...}) = perspective;
    5.14  fun set_perspective ids =
     6.1 --- a/src/Pure/PIDE/document.scala	Tue Feb 26 20:11:11 2013 +0100
     6.2 +++ b/src/Pure/PIDE/document.scala	Wed Feb 27 12:45:19 2013 +0100
     6.3 @@ -40,7 +40,7 @@
     6.4      sealed case class Header(
     6.5        imports: List[Name],
     6.6        keywords: Thy_Header.Keywords,
     6.7 -      uses: List[(String, Boolean)],
     6.8 +      files: List[String],
     6.9        errors: List[String] = Nil)
    6.10      {
    6.11        def error(msg: String): Header = copy(errors = errors ::: List(msg))
     7.1 --- a/src/Pure/PIDE/protocol.ML	Tue Feb 26 20:11:11 2013 +0100
     7.2 +++ b/src/Pure/PIDE/protocol.ML	Wed Feb 27 12:45:19 2013 +0100
     7.3 @@ -37,16 +37,16 @@
     7.4                    fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
     7.5                    fn ([], a) =>
     7.6                      let
     7.7 -                      val (master, (name, (imports, (keywords, (uses, errors))))) =
     7.8 +                      val (master, (name, (imports, (keywords, (files, errors))))) =
     7.9                          pair string (pair string (pair (list string)
    7.10                            (pair (list (pair string
    7.11                              (option (pair (pair string (list string)) (list string)))))
    7.12 -                            (pair (list (pair string bool)) (list string))))) a;
    7.13 +                            (pair (list string) (list string))))) a;
    7.14                        val imports' = map (rpair Position.none) imports;
    7.15 -                      val (uses', errors') =
    7.16 -                        (map (apfst Path.explode) uses, errors)
    7.17 +                      val (files', errors') =
    7.18 +                        (map Path.explode files, errors)
    7.19                            handle ERROR msg => ([], errors @ [msg]);
    7.20 -                      val header = Thy_Header.make (name, Position.none) imports' keywords uses';
    7.21 +                      val header = Thy_Header.make (name, Position.none) imports' keywords files';
    7.22                      in Document.Deps (master, header, errors') end,
    7.23                    fn (a, []) => Document.Perspective (map int_atom a)]))
    7.24              end;
     8.1 --- a/src/Pure/PIDE/protocol.scala	Tue Feb 26 20:11:11 2013 +0100
     8.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Feb 27 12:45:19 2013 +0100
     8.3 @@ -290,13 +290,13 @@
     8.4                val imports = header.imports.map(_.node)
     8.5                val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
     8.6                // FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
     8.7 -              val uses = header.uses
     8.8 +              val files = header.files
     8.9                (Nil,
    8.10                  pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
    8.11                    pair(list(pair(Encode.string,
    8.12                      option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
    8.13 -                  pair(list(pair(Encode.string, bool)), list(Encode.string))))))(
    8.14 -                (dir, (name.theory, (imports, (keywords, (uses, header.errors))))))) },
    8.15 +                  pair(list(Encode.string), list(Encode.string))))))(
    8.16 +                (dir, (name.theory, (imports, (keywords, (files, header.errors))))))) },
    8.17            { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
    8.18        def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
    8.19        {
     9.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Feb 26 20:11:11 2013 +0100
     9.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Feb 27 12:45:19 2013 +0100
     9.3 @@ -592,10 +592,9 @@
     9.4  
     9.5          fun filerefs f =
     9.6              let val thy = thy_name f
     9.7 -                val filerefs = map #1 (#uses (Thy_Load.check_thy (Path.dir f) thy))
     9.8              in
     9.9                  issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
    9.10 -                                     name=NONE, idtables=[], fileurls=filerefs})
    9.11 +                                     name=NONE, idtables=[], fileurls=[]})
    9.12              end
    9.13  
    9.14          fun thyrefs thy =
    10.1 --- a/src/Pure/Pure.thy	Tue Feb 26 20:11:11 2013 +0100
    10.2 +++ b/src/Pure/Pure.thy	Wed Feb 27 12:45:19 2013 +0100
    10.3 @@ -12,8 +12,7 @@
    10.4      "attach" "begin" "binder" "constrains" "defines" "fixes" "for"
    10.5      "identifier" "if" "imports" "in" "includes" "infix" "infixl"
    10.6      "infixr" "is" "keywords" "notes" "obtains" "open" "output"
    10.7 -    "overloaded" "pervasive" "shows" "structure" "unchecked" "uses"
    10.8 -    "where" "|"
    10.9 +    "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
   10.10    and "header" :: diag
   10.11    and "chapter" :: thy_heading1
   10.12    and "section" :: thy_heading2
    11.1 --- a/src/Pure/Thy/present.ML	Tue Feb 26 20:11:11 2013 +0100
    11.2 +++ b/src/Pure/Thy/present.ML	Wed Feb 27 12:45:19 2013 +0100
    11.3 @@ -21,7 +21,7 @@
    11.4    val init_theory: string -> unit
    11.5    val theory_source: string -> (unit -> HTML.text) -> unit
    11.6    val theory_output: string -> string -> unit
    11.7 -  val begin_theory: int -> Path.T -> (Path.T * bool) list -> theory -> theory
    11.8 +  val begin_theory: int -> Path.T -> theory -> theory
    11.9    val drafts: string -> Path.T list -> Path.T
   11.10  end;
   11.11  
   11.12 @@ -451,13 +451,14 @@
   11.13          else Url.File (Path.append (mk_rel_path curr_session session) (html_path name)));
   11.14    in (link, name) end;
   11.15  
   11.16 -fun begin_theory update_time dir files thy =
   11.17 +fun begin_theory update_time dir thy =
   11.18      session_default thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
   11.19    let
   11.20      val name = Context.theory_name thy;
   11.21      val parents = Theory.parents_of thy;
   11.22      val parent_specs = map (parent_link remote_path path) parents;
   11.23  
   11.24 +    val files = [];  (* FIXME *)
   11.25      val files_html = files |> map (fn (raw_path, loadit) =>
   11.26        let
   11.27          val path = File.check_file (File.full_path dir raw_path);
    12.1 --- a/src/Pure/Thy/thy_header.ML	Tue Feb 26 20:11:11 2013 +0100
    12.2 +++ b/src/Pure/Thy/thy_header.ML	Wed Feb 27 12:45:19 2013 +0100
    12.3 @@ -11,9 +11,8 @@
    12.4     {name: string * Position.T,
    12.5      imports: (string * Position.T) list,
    12.6      keywords: keywords,
    12.7 -    uses: (Path.T * bool) list}
    12.8 -  val make: string * Position.T -> (string * Position.T) list -> keywords ->
    12.9 -    (Path.T * bool) list -> header
   12.10 +    files: Path.T list}
   12.11 +  val make: string * Position.T -> (string * Position.T) list -> keywords -> Path.T list -> header
   12.12    val define_keywords: header -> unit
   12.13    val declare_keyword: string * Keyword.spec option -> theory -> theory
   12.14    val the_keyword: theory -> string -> Keyword.spec option
   12.15 @@ -31,10 +30,10 @@
   12.16   {name: string * Position.T,
   12.17    imports: (string * Position.T) list,
   12.18    keywords: keywords,
   12.19 -  uses: (Path.T * bool) list};
   12.20 +  files: Path.T list};
   12.21  
   12.22 -fun make name imports keywords uses : header =
   12.23 -  {name = name, imports = imports, keywords = keywords, uses = uses};
   12.24 +fun make name imports keywords files : header =
   12.25 +  {name = name, imports = imports, keywords = keywords, files = files};
   12.26  
   12.27  
   12.28  
   12.29 @@ -73,12 +72,11 @@
   12.30  val theoryN = "theory";
   12.31  val importsN = "imports";
   12.32  val keywordsN = "keywords";
   12.33 -val usesN = "uses";
   12.34  val beginN = "begin";
   12.35  
   12.36  val header_lexicons =
   12.37    pairself (Scan.make_lexicon o map Symbol.explode)
   12.38 -   (["%", "(", ")", ",", "::", ";", "==", "and", beginN, importsN, keywordsN, usesN],
   12.39 +   (["%", "(", ")", ",", "::", ";", "==", "and", beginN, importsN, keywordsN],
   12.40      [headerN, theoryN]);
   12.41  
   12.42  
   12.43 @@ -86,7 +84,6 @@
   12.44  
   12.45  local
   12.46  
   12.47 -val file_name = Parse.group (fn () => "file name") Parse.path >> Path.explode;
   12.48  val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name);
   12.49  
   12.50  val opt_files =
   12.51 @@ -107,19 +104,14 @@
   12.52  
   12.53  val keyword_decls = Parse.and_list1 keyword_decl >> flat;
   12.54  
   12.55 -val file =
   12.56 -  Parse.$$$ "(" |-- Parse.!!! (file_name --| Parse.$$$ ")") >> rpair false ||
   12.57 -  file_name >> rpair true;
   12.58 -
   12.59  in
   12.60  
   12.61  val args =
   12.62    theory_name --
   12.63    Scan.optional (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) [] --
   12.64 -  Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --
   12.65 -  Scan.optional (Parse.$$$ usesN |-- Parse.!!! (Scan.repeat1 file)) [] --|
   12.66 +  Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
   12.67    Parse.$$$ beginN >>
   12.68 -  (fn (((name, imports), keywords), uses) => make name imports keywords uses);
   12.69 +  (fn ((name, imports), keywords) => make name imports keywords []);
   12.70  
   12.71  end;
   12.72  
    13.1 --- a/src/Pure/Thy/thy_header.scala	Tue Feb 26 20:11:11 2013 +0100
    13.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Feb 27 12:45:19 2013 +0100
    13.3 @@ -22,12 +22,11 @@
    13.4    val IMPORTS = "imports"
    13.5    val KEYWORDS = "keywords"
    13.6    val AND = "and"
    13.7 -  val USES = "uses"
    13.8    val BEGIN = "begin"
    13.9  
   13.10    private val lexicon =
   13.11      Scan.Lexicon("%", "(", ")", ",", "::", ";", "==",
   13.12 -      AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY, USES)
   13.13 +      AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY)
   13.14  
   13.15  
   13.16    /* theory file name */
   13.17 @@ -72,9 +71,8 @@
   13.18        theory_name ~
   13.19        (opt(keyword(IMPORTS) ~! (rep1(theory_name))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
   13.20        (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
   13.21 -      (opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
   13.22        keyword(BEGIN) ^^
   13.23 -      { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
   13.24 +      { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs, Nil) }
   13.25  
   13.26      (keyword(HEADER) ~ tags) ~!
   13.27        ((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
   13.28 @@ -120,9 +118,9 @@
   13.29    name: String,
   13.30    imports: List[String],
   13.31    keywords: Thy_Header.Keywords,
   13.32 -  uses: List[(String, Boolean)])
   13.33 +  files: List[String])
   13.34  {
   13.35    def map(f: String => String): Thy_Header =
   13.36 -    Thy_Header(f(name), imports.map(f), keywords, uses.map(p => (f(p._1), p._2)))
   13.37 +    Thy_Header(f(name), imports.map(f), keywords, files.map(f))
   13.38  }
   13.39  
    14.1 --- a/src/Pure/Thy/thy_info.ML	Tue Feb 26 20:11:11 2013 +0100
    14.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Feb 27 12:45:19 2013 +0100
    14.3 @@ -235,7 +235,7 @@
    14.4  fun required_by _ [] = ""
    14.5    | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
    14.6  
    14.7 -fun load_thy last_timing initiators update_time deps text (name, pos) uses keywords parents =
    14.8 +fun load_thy last_timing initiators update_time deps text (name, pos) keywords parents =
    14.9    let
   14.10      val _ = kill_thy name;
   14.11      val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
   14.12 @@ -243,7 +243,7 @@
   14.13  
   14.14      val {master = (thy_path, _), imports} = deps;
   14.15      val dir = Path.dir thy_path;
   14.16 -    val header = Thy_Header.make (name, pos) imports keywords uses;
   14.17 +    val header = Thy_Header.make (name, pos) imports keywords [];
   14.18  
   14.19      val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
   14.20  
   14.21 @@ -257,21 +257,21 @@
   14.22  
   14.23  fun check_deps dir name =
   14.24    (case lookup_deps name of
   14.25 -    SOME NONE => (true, NONE, Position.none, get_imports name, [], [])
   14.26 +    SOME NONE => (true, NONE, Position.none, get_imports name, [])
   14.27    | NONE =>
   14.28 -      let val {master, text, theory_pos, imports, keywords, uses} = Thy_Load.check_thy dir name
   14.29 -      in (false, SOME (make_deps master imports, text), theory_pos, imports, uses, keywords) end
   14.30 +      let val {master, text, theory_pos, imports, keywords} = Thy_Load.check_thy dir name
   14.31 +      in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end
   14.32    | SOME (SOME {master, ...}) =>
   14.33        let
   14.34          val {master = master', text = text', theory_pos = theory_pos', imports = imports',
   14.35 -          uses = uses', keywords = keywords'} = Thy_Load.check_thy dir name;
   14.36 +          keywords = keywords'} = Thy_Load.check_thy dir name;
   14.37          val deps' = SOME (make_deps master' imports', text');
   14.38          val current =
   14.39            #2 master = #2 master' andalso
   14.40              (case lookup_theory name of
   14.41                NONE => false
   14.42              | SOME theory => Thy_Load.load_current theory);
   14.43 -      in (current, deps', theory_pos', imports', uses', keywords') end);
   14.44 +      in (current, deps', theory_pos', imports', keywords') end);
   14.45  
   14.46  in
   14.47  
   14.48 @@ -289,7 +289,7 @@
   14.49            val dir' = Path.append dir (Path.dir path);
   14.50            val _ = member (op =) initiators name andalso error (cycle_msg initiators);
   14.51  
   14.52 -          val (current, deps, theory_pos, imports, uses, keywords) = check_deps dir' name
   14.53 +          val (current, deps, theory_pos, imports, keywords) = check_deps dir' name
   14.54              handle ERROR msg => cat_error msg
   14.55                (loader_msg "the error(s) above occurred while examining theory" [name] ^
   14.56                  Position.here require_pos ^ required_by "\n" initiators);
   14.57 @@ -310,7 +310,7 @@
   14.58                      val update_time = serial ();
   14.59                      val load =
   14.60                        load_thy last_timing initiators update_time dep
   14.61 -                        text (name, theory_pos) uses keywords;
   14.62 +                        text (name, theory_pos) keywords;
   14.63                    in Task (parents, load) end);
   14.64  
   14.65            val tasks'' = new_entry name parents task tasks';
    15.1 --- a/src/Pure/Thy/thy_info.scala	Tue Feb 26 20:11:11 2013 +0100
    15.2 +++ b/src/Pure/Thy/thy_info.scala	Wed Feb 27 12:45:19 2013 +0100
    15.3 @@ -94,7 +94,7 @@
    15.4                  Library.future_value(Exn.capture {
    15.5                    try {
    15.6                      val files = thy_load.body_files(syntax0, string)
    15.7 -                    header0.copy(uses = header0.uses ::: files.map((_, false)))
    15.8 +                    header0.copy(files = header0.files ::: files)
    15.9                    }
   15.10                    catch { case ERROR(msg) => err(msg) }
   15.11                  })
    16.1 --- a/src/Pure/Thy/thy_load.ML	Tue Feb 26 20:11:11 2013 +0100
    16.2 +++ b/src/Pure/Thy/thy_load.ML	Wed Feb 27 12:45:19 2013 +0100
    16.3 @@ -12,7 +12,7 @@
    16.4    val parse_files: string -> (theory -> Token.file list) parser
    16.5    val check_thy: Path.T -> string ->
    16.6     {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
    16.7 -    imports: (string * Position.T) list, uses: (Path.T * bool) list, keywords: Thy_Header.keywords}
    16.8 +    imports: (string * Position.T) list, keywords: Thy_Header.keywords}
    16.9    val provide: Path.T * SHA1.digest -> theory -> theory
   16.10    val provide_parse_files: string -> (theory -> Token.file list * theory) parser
   16.11    val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
   16.12 @@ -132,13 +132,13 @@
   16.13      val master_file = check_file dir path;
   16.14      val text = File.read master_file;
   16.15  
   16.16 -    val {name = (name, pos), imports, uses, keywords} =
   16.17 +    val {name = (name, pos), imports, files = [], keywords} =
   16.18        Thy_Header.read (Path.position master_file) text;
   16.19      val _ = thy_name <> name andalso
   16.20        error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos);
   16.21    in
   16.22     {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
   16.23 -    imports = imports, uses = uses, keywords = keywords}
   16.24 +    imports = imports, keywords = keywords}
   16.25    end;
   16.26  
   16.27  
   16.28 @@ -207,11 +207,10 @@
   16.29  
   16.30  (* load_thy *)
   16.31  
   16.32 -fun begin_theory master_dir {name, imports, keywords, uses} parents =
   16.33 +fun begin_theory master_dir {name, imports, keywords, files = []} parents =
   16.34    Theory.begin_theory name parents
   16.35    |> put_deps master_dir imports
   16.36    |> fold Thy_Header.declare_keyword keywords
   16.37 -  |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
   16.38    |> Theory.checkpoint;
   16.39  
   16.40  fun excursion last_timing init elements =
   16.41 @@ -239,12 +238,12 @@
   16.42    let
   16.43      val time = ! Toplevel.timing;
   16.44  
   16.45 -    val {name = (name, _), uses, ...} = header;
   16.46 +    val {name = (name, _), files = [], ...} = header;
   16.47      val _ = Thy_Header.define_keywords header;
   16.48      val _ = Present.init_theory name;
   16.49      fun init () =
   16.50        begin_theory master_dir header parents
   16.51 -      |> Present.begin_theory update_time master_dir uses;
   16.52 +      |> Present.begin_theory update_time master_dir;
   16.53  
   16.54      val lexs = Keyword.get_lexicons ();
   16.55  
    17.1 --- a/src/Pure/Thy/thy_load.scala	Tue Feb 26 20:11:11 2013 +0100
    17.2 +++ b/src/Pure/Thy/thy_load.scala	Wed Feb 27 12:45:19 2013 +0100
    17.3 @@ -114,8 +114,7 @@
    17.4            " for theory " + quote(name1))
    17.5  
    17.6        val imports = header.imports.map(import_name(name.dir, _))
    17.7 -      val uses = header.uses
    17.8 -      Document.Node.Header(imports, header.keywords, uses)
    17.9 +      Document.Node.Header(imports, header.keywords, Nil)
   17.10      }
   17.11      catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
   17.12    }
    18.1 --- a/src/Pure/Tools/build.scala	Tue Feb 26 20:11:11 2013 +0100
    18.2 +++ b/src/Pure/Tools/build.scala	Wed Feb 27 12:45:19 2013 +0100
    18.3 @@ -417,9 +417,9 @@
    18.4            val all_files =
    18.5              (thy_deps.deps.map({ case dep =>
    18.6                val thy = Path.explode(dep.name.node)
    18.7 -              val uses = dep.join_header.uses.map(p =>
    18.8 -                Path.explode(dep.name.dir) + Path.explode(p._1))
    18.9 -              thy :: uses
   18.10 +              val files = dep.join_header.files.map(file =>
   18.11 +                Path.explode(dep.name.dir) + Path.explode(file))
   18.12 +              thy :: files
   18.13              }).flatten ::: info.files.map(file => info.dir + file)).map(_.expand)
   18.14  
   18.15            if (list_files)