--- a/src/Pure/Thy/thy_load.ML Sat Nov 16 16:57:09 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML Sat Nov 16 17:04:17 2013 +0100
@@ -16,7 +16,6 @@
val provide: Path.T * SHA1.digest -> theory -> theory
val provide_parse_files: string -> (theory -> Token.file list * theory) parser
val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
- val use_file: Path.T -> theory -> string * theory
val loaded_files: theory -> Path.T list
val loaded_files_current: theory -> bool
val use_ml: Path.T -> unit
@@ -164,12 +163,6 @@
val id = SHA1.digest text;
in ((full_path, id), text) end;
-fun use_file src_path thy =
- let
- val ((_, id), text) = load_file thy src_path;
- val thy' = provide (src_path, id) thy;
- in (text, thy') end;
-
(*Proof General legacy*)
fun loaded_files thy =
let val {master_dir, provided, ...} = Files.get thy