diff -r a033b5b6f544 -r 3a196e63a80d src/Pure/term.ML
--- a/src/Pure/term.ML	Sat Aug 03 13:12:58 2024 +0200
+++ b/src/Pure/term.ML	Sun Aug 04 12:21:13 2024 +0200
@@ -38,6 +38,8 @@
   val is_TFree: typ -> bool
   val is_TVar: typ -> bool
   val dest_Type: typ -> string * typ list
+  val dest_Type_name: typ -> string
+  val dest_Type_args: typ -> typ list
   val dest_TFree: typ -> string * sort
   val dest_TVar: typ -> indexname * sort
   val is_Bound: term -> bool
@@ -282,6 +284,9 @@
 fun dest_Type (Type x) = x
   | dest_Type T = raise TYPE ("dest_Type", [T], []);
 
+val dest_Type_name = #1 o dest_Type;
+val dest_Type_args = #2 o dest_Type;
+
 fun dest_TFree (TFree x) = x
   | dest_TFree T = raise TYPE ("dest_TFree", [T], []);