# HG changeset patch
# User wenzelm
# Date 1708600933 -3600
# Node ID ecc851dd274f549c7200b0d7b6974e78122ff841
# Parent  fabe9f89911f69d5142fbe86cdd8118726cf53b8
unused;

diff -r fabe9f89911f -r ecc851dd274f src/Pure/ML/ml_heap.scala
--- a/src/Pure/ML/ml_heap.scala	Thu Feb 22 12:19:23 2024 +0100
+++ b/src/Pure/ML/ml_heap.scala	Thu Feb 22 12:22:13 2024 +0100
@@ -7,11 +7,6 @@
 package isabelle
 
 
-import java.nio.ByteBuffer
-import java.nio.channels.FileChannel
-import java.nio.file.StandardOpenOption
-
-
 object ML_Heap {
   /** heap file with SHA1 digest **/