# HG changeset patch
# User wenzelm
# Date 1735482868 -3600
# Node ID 6e19d0ebff8a3e15c2e29c3e1a21b90755cc1b2a
# Parent  6c3de898b055769998d2684212116151b05991e6
unused;

diff -r 6c3de898b055 -r 6e19d0ebff8a src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sun Dec 29 15:15:06 2024 +0100
+++ b/src/Pure/General/pretty.ML	Sun Dec 29 15:34:28 2024 +0100
@@ -343,12 +343,6 @@
   pos = 0,
   nl = 0};
 
-fun newline s {tx, ind = _, pos = _, nl} : text =
- {tx = Bytes.add s tx,
-  ind = Buffer.empty,
-  pos = 0,
-  nl = nl + 1};
-
 fun string (s, len) {tx, ind, pos: int, nl} : text =
  {tx = Bytes.add s tx,
   ind = Buffer.add s ind,