# HG changeset patch
# User wenzelm
# Date 1703873110 -3600
# Node ID e7796c55d8408f64a37bb66c3f21c9c541aef133
# Parent  b9d80d5aca8ed835bfc8d0475cd76f138e8ecedc
more operations;

diff -r b9d80d5aca8e -r e7796c55d840 src/Pure/term.ML
--- 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 **)