# HG changeset patch
# User wenzelm
# Date 1384617857 -3600
# Node ID 7110476960f732fd8a30e5850604665dcf88a8c0
# Parent  019394de2b41948dd99340eda4fdc0880eb5c9fd
obsolete;

diff -r 019394de2b41 -r 7110476960f7 src/Pure/Thy/thy_load.ML
--- 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