# HG changeset patch
# User wenzelm
# Date 1695728228 -7200
# Node ID f34a451f7b5b63f88d0e5320a0d1a4f7ff2aaae1
# Parent  1eca7abaa0159552cf45a670736e09fb7c3f978f
tuned;

diff -r 1eca7abaa015 -r f34a451f7b5b src/Pure/General/file_stream.ML
--- a/src/Pure/General/file_stream.ML	Tue Sep 26 13:34:04 2023 +0200
+++ b/src/Pure/General/file_stream.ML	Tue Sep 26 13:37:08 2023 +0200
@@ -31,7 +31,8 @@
     let
       val file = open_file path;
       val result = Exn.capture (run f) file;
-    in close_file file; Exn.release result end);
+      val _ = close_file file;
+    in Exn.release result end);
 
 in
 
diff -r 1eca7abaa015 -r f34a451f7b5b src/Pure/General/socket_io.ML
--- a/src/Pure/General/socket_io.ML	Tue Sep 26 13:34:04 2023 +0200
+++ b/src/Pure/General/socket_io.ML	Tue Sep 26 13:37:08 2023 +0200
@@ -92,7 +92,9 @@
     let
       val streams = open_streams socket_name;
       val result = Exn.capture (run f) streams;
-    in BinIO.closeIn (#1 streams); BinIO.closeOut (#2 streams); Exn.release result end);
+      val _ = BinIO.closeIn (#1 streams);
+      val _ = BinIO.closeOut (#2 streams);
+    in Exn.release result end);
 
 fun with_streams' f socket_name password =
   with_streams (fn streams =>