1.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed May 12 16:52:28 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed May 12 16:54:31 1999 +0200
     1.3 @@ -198,7 +198,7 @@
     1.4  
     1.5  fun deps_thy name ml path =
     1.6    let
     1.7 -    val src = Source.of_file path;
     1.8 +    val src = File.source path;
     1.9      val is_old = warn_theory_style path (is_old_theory src);
    1.10      val (name', parents, files) =
    1.11        (*Note: old style headers dynamically depend on the current lexicon :-( *)
    1.12 @@ -248,7 +248,7 @@
    1.13    end;
    1.14  
    1.15  fun run_thy name path =
    1.16 -  let val (src, pos) = Source.of_file path in
    1.17 +  let val (src, pos) = File.source path in
    1.18      Present.theory_source name src;
    1.19      if is_old_theory (src, pos) then ThySyn.load_thy name (Source.exhaust src)
    1.20      else (Toplevel.excursion (parse_thy (src, pos))

     2.1 --- a/src/Pure/Isar/session.ML	Wed May 12 16:52:28 1999 +0200
     2.2 +++ b/src/Pure/Isar/session.ML	Wed May 12 16:54:31 1999 +0200
     2.3 @@ -61,7 +61,7 @@
     2.4  fun use_dir reset info parent name =
     2.5    (init reset parent name;
     2.6      Present.init info (path ()) name;
     2.7 -    Symbol.use root_file;
     2.8 +    File.symbol_use root_file;
     2.9      finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1);
    2.10  
    2.11  

     3.1 --- a/src/Pure/Thy/thy_load.ML	Wed May 12 16:52:28 1999 +0200
     3.2 +++ b/src/Pure/Thy/thy_load.ML	Wed May 12 16:54:31 1999 +0200
     3.3 @@ -75,7 +75,7 @@
     3.4  fun load_file raw_path =
     3.5    (case check_file raw_path of
     3.6      None => error ("Could not find ML file " ^ quote (Path.pack raw_path))
     3.7 -  | Some (path, info) => (Symbol.use path; (path, info)));
     3.8 +  | Some (path, info) => (File.symbol_use path; (path, info)));
     3.9  
    3.10  
    3.11  (* check_thy *)

     4.1 --- a/src/Pure/Thy/thy_syn.ML	Wed May 12 16:52:28 1999 +0200
     4.2 +++ b/src/Pure/Thy/thy_syn.ML	Wed May 12 16:54:31 1999 +0200
     4.3 @@ -55,7 +55,7 @@
     4.4      val txt_out = ThyParse.parse_thy (! syntax) chs;
     4.5    in
     4.6      File.write tmp_path txt_out;
     4.7 -    Symbol.use tmp_path;
     4.8 +    File.symbol_use tmp_path;
     4.9      if ! delete_tmpfiles then File.rm tmp_path else ()
    4.10    end;
    4.11