# HG changeset patch
# User wenzelm
# Date 1725882208 -7200
# Node ID 0d92bd90be6c3627c542c66099c84bf365ad3a9d
# Parent  fb0a9fc3901fc795d4af695106698300b83cebff
discontinued unused global variable (see also following bf465f335e85);

diff -r fb0a9fc3901f -r 0d92bd90be6c src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Mon Sep 09 11:41:31 2024 +0200
+++ b/src/Pure/General/pretty.ML	Mon Sep 09 13:43:28 2024 +0200
@@ -66,7 +66,6 @@
   val big_list: string -> T list -> T
   val indent: int -> T -> T
   val unbreakable: T -> T
-  val margin_default: int Unsynchronized.ref
   val regularN: string
   val symbolicN: string
   val output_buffer: int option -> T -> Buffer.T
@@ -397,15 +396,13 @@
 
 (* output interfaces *)
 
-val margin_default = Unsynchronized.ref ML_Pretty.default_margin;  (*right margin, or page width*)
-
 val regularN = "pretty_regular";
 val symbolicN = "pretty_symbolic";
 
 fun output_buffer margin prt =
   if print_mode_active symbolicN andalso not (print_mode_active regularN)
   then symbolic prt
-  else format_tree (the_default (! margin_default) margin) prt;
+  else format_tree (the_default ML_Pretty.default_margin margin) prt;
 
 val output = Buffer.contents oo output_buffer;
 fun string_of_margin margin = implode o Output.escape o output (SOME margin);