unused;
authorwenzelm
Wed, 11 Sep 2024 23:07:18 +0200
changeset 80865 7c20c207af48
parent 80864 1b1f77bcee5f
child 80866 8c67b14fdd48
unused;
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);