src/Pure/term.ML

   val dest_Free: term -> string * typ
   val dest_Var: term -> indexname * typ
   val dest_comb: term -> term * term
   val domain_type: typ -> typ
   val range_type: typ -> typ
+  val dest_funT: typ -> typ * typ
   val binder_types: typ -> typ list
   val body_type: typ -> typ
   val strip_type: typ -> typ list * typ
   val type_of1: typ list * term -> typ
   val type_of: term -> typ

 
 
 fun domain_type (Type("fun", [T,_])) = T
 and range_type  (Type("fun", [_,T])) = T;
 
+fun dest_funT (Type ("fun", [T, U])) = (T, U)
+  | dest_funT T = raise TYPE ("dest_funT", [T], []);
+
+
 (* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
 fun binder_types (Type("fun",[S,T])) = S :: binder_types T
   | binder_types _   =  [];
 
 (* maps  [T1,...,Tn]--->T  to T*)