--- a/src/Pure/term.ML Mon Jan 08 21:54:20 2024 +0100
+++ b/src/Pure/term.ML Mon Jan 08 22:26:04 2024 +0100
@@ -151,6 +151,8 @@
val declare_term_frees: term -> Name.context -> Name.context
val variant_frees: term -> (string * 'a) list -> (string * 'a) list
val smash_sortsT_same: sort -> typ Same.operation
+ val smash_sortsT: sort -> typ -> typ
+ val smash_sorts: sort -> term -> term
val strip_sortsT_same: typ Same.operation
val strip_sortsT: typ -> typ
val strip_sorts: term -> term
@@ -590,6 +592,9 @@
(fn TFree (x, S) => if S = S' then raise Same.SAME else TFree (x, S')
| TVar (xi, S) => if S = S' then raise Same.SAME else TVar (xi, S'));
+val smash_sortsT = Same.commit o smash_sortsT_same;
+val smash_sorts = map_types o smash_sortsT_same;
+
val strip_sortsT_same = smash_sortsT_same [];
val strip_sortsT = Same.commit strip_sortsT_same;
val strip_sorts = map_types strip_sortsT_same;