# HG changeset patch
# User wenzelm
# Date 897755139 -7200
# Node ID e00ac9db997513e159976fbbf1fbb98c21b2ffe9
# Parent  95f6daba7a9d19d5631c43c24dbf024d81568734
removed use_text;

diff -r 95f6daba7a9d -r e00ac9db9975 src/Pure/Thy/use.ML
--- a/src/Pure/Thy/use.ML	Fri Jun 12 18:08:41 1998 +0200
+++ b/src/Pure/Thy/use.ML	Sat Jun 13 18:25:39 1998 +0200
@@ -9,7 +9,6 @@
 
 signature USE =
 sig
-  val use_text: string -> string -> unit
   val use: string -> unit
   val exit_use: string -> unit
   val time_use: string -> unit
@@ -19,22 +18,6 @@
 structure Use: USE =
 struct
 
-
-(* use_text *)
-
-val use_orig = use;
-
-fun use_text name txt =
-  let
-    val tmp_name = File.tmp_name ("." ^ Path.base_name name);
-    val _ = File.write tmp_name txt;
-    val rm = OS.FileSys.remove;
-  in
-    use_orig tmp_name handle exn => (rm tmp_name; raise exn);
-    rm tmp_name
-  end;
-
-
 (* generate suffix *)
 
 fun append_suffix name =
@@ -48,6 +31,8 @@
 
 (* input filtering *)
 
+val use_orig = use;
+
 val use_filter =
   if not needs_filtered_use then use_orig
   else
@@ -57,7 +42,15 @@
         val txt_out = Symbol.input txt;
       in
         if txt = txt_out then use_orig name
-        else use_text name txt_out
+        else
+          let
+            val tmp_name = File.tmp_name ("." ^ Path.base_name name);
+            val _ = File.write tmp_name txt_out;
+            val rm = OS.FileSys.remove;
+          in
+            use_orig tmp_name handle exn => (rm tmp_name; raise exn);
+            rm tmp_name
+          end
       end;