# HG changeset patch
# User wenzelm
# Date 1680025234 -7200
# Node ID c4c96a833a3732870dd566109bc5b3e46f85d1a1
# Parent  59c94a376a3c2eb3865e5feaf595914825016260
tuned;

diff -r 59c94a376a3c -r c4c96a833a37 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Tue Mar 28 19:07:58 2023 +0200
+++ b/src/Pure/envir.ML	Tue Mar 28 19:40:34 2023 +0200
@@ -94,7 +94,7 @@
 
 
 (*NB: type unification may invent new sorts*)  (* FIXME tenv!? *)
-val insert_sorts = Vartab.fold (fn (_, (_, T)) => Sortset.insert_typ T) o type_env;
+val insert_sorts = Vartab.fold (Sortset.insert_typ o #2 o #2) o type_env;
 
 (*Generate a list of distinct variables.
   Increments index to make them distinct from ALL present variables. *)