Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Tue, 28 Mar 2023 19:40:34 +0200
changeset 77734 c4c96a833a37
parent 77733 59c94a376a3c
child 77735 be3f838b3e17
tuned;
src/Pure/envir.ML file | annotate | diff | comparison | revisions 
--- 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. *)
isabelle