obsolete;
authorwenzelm
Sat Nov 16 17:04:17 2013 +0100 (2013-11-16)
changeset 544487110476960f7
parent 54447 019394de2b41
child 54449 f3cfe882f9af
obsolete;
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Thy/thy_load.ML	Sat Nov 16 16:57:09 2013 +0100
     1.2 +++ b/src/Pure/Thy/thy_load.ML	Sat Nov 16 17:04:17 2013 +0100
     1.3 @@ -16,7 +16,6 @@
     1.4    val provide: Path.T * SHA1.digest -> theory -> theory
     1.5    val provide_parse_files: string -> (theory -> Token.file list * theory) parser
     1.6    val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
     1.7 -  val use_file: Path.T -> theory -> string * theory
     1.8    val loaded_files: theory -> Path.T list
     1.9    val loaded_files_current: theory -> bool
    1.10    val use_ml: Path.T -> unit
    1.11 @@ -164,12 +163,6 @@
    1.12      val id = SHA1.digest text;
    1.13    in ((full_path, id), text) end;
    1.14  
    1.15 -fun use_file src_path thy =
    1.16 -  let
    1.17 -    val ((_, id), text) = load_file thy src_path;
    1.18 -    val thy' = provide (src_path, id) thy;
    1.19 -  in (text, thy') end;
    1.20 -
    1.21  (*Proof General legacy*)
    1.22  fun loaded_files thy =
    1.23    let val {master_dir, provided, ...} = Files.get thy