--- a/src/Pure/term.ML Fri Dec 29 19:00:17 2023 +0100
+++ b/src/Pure/term.ML Fri Dec 29 19:05:10 2023 +0100
@@ -122,6 +122,7 @@
signature TERM =
sig
include BASIC_TERM
+ val dest_atyp_sort: typ -> sort
val aT: sort -> typ
val itselfT: typ -> typ
val a_itselfT: typ
@@ -279,6 +280,10 @@
fun dest_TVar (TVar x) = x
| dest_TVar T = raise TYPE ("dest_TVar", [T], []);
+fun dest_atyp_sort (TFree (_, S)) = S
+ | dest_atyp_sort (TVar (_, S)) = S
+ | dest_atyp_sort T = raise TYPE ("dest_atyp_sort", [T], []);
+
(** Discriminators **)