--- a/src/Pure/term.ML Fri Dec 29 19:22:15 2023 +0100
+++ b/src/Pure/term.ML Fri Dec 29 20:01:04 2023 +0100
@@ -122,7 +122,6 @@
signature TERM =
sig
include BASIC_TERM
- val dest_atyp_sort: typ -> sort
val aT: sort -> typ
val itselfT: typ -> typ
val a_itselfT: typ
@@ -280,10 +279,6 @@
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 **)