# HG changeset patch
# User wenzelm
# Date 1721381305 -7200
# Node ID 41957635424914a062b4f6818af7c6ded06b9af0
# Parent  12de235f8b927a124402ebb3757dbbbdb3e09347
tuned whitespace;

diff -r 12de235f8b92 -r 419576354249 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Thu Jul 18 17:02:39 2024 +0200
+++ b/src/Pure/zterm.ML	Fri Jul 19 11:28:25 2024 +0200
@@ -1427,4 +1427,4 @@
 
 end;
 
-end;
\ No newline at end of file
+end;