# HG changeset patch
# User wenzelm
# Date 1726088838 -7200
# Node ID 7c20c207af48b3f1094d0302814c6dab33ad11ca
# Parent  1b1f77bcee5f17bcbc6bae1da96eb97127f9d09a
unused;

diff -r 1b1f77bcee5f -r 7c20c207af48 src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Wed Sep 11 22:56:42 2024 +0200
+++ b/src/Pure/General/print_mode.ML	Wed Sep 11 23:07:18 2024 +0200
@@ -24,7 +24,6 @@
   val latex: string
   val setmp: string list -> ('a -> 'b) -> 'a -> 'b
   val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
-  val closure: ('a -> 'b) -> 'a -> 'b
   val add_modes: string list -> unit
 end;
 
@@ -52,7 +51,6 @@
 fun setmp modes f x = Thread_Data.setmp print_mode_var (SOME modes) f x;
 
 fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
-fun closure f = with_modes [] f;
 
 fun add_modes modes = Unsynchronized.change print_mode (append modes);