src/Pure/Thy/use.ML

 required).
 *)
 
 signature USE =
 sig
-  val use_text: string -> string -> unit
   val use: string -> unit
   val exit_use: string -> unit
   val time_use: string -> unit
   val cd: string -> unit
 end;
 
 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 =
   let

   in try ["", ".ML", ".sml"] end;
 
 
 (* input filtering *)
 
+val use_orig = use;
+
 val use_filter =
   if not needs_filtered_use then use_orig
   else
     fn name =>
       let
         val txt = File.read name;
         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;
 
 
 (* use commands *)