src/Pure/term.ML
changeset 4464 7a8150506746
parent 4444 fa05a79b3e97
child 4480 d26e28c52788
--- a/src/Pure/term.ML	Mon Dec 22 12:21:37 1997 +0100
+++ b/src/Pure/term.ML	Mon Dec 22 12:22:06 1997 +0100
@@ -254,7 +254,8 @@
   | dest_Var t = raise TERM("dest_Var", [t]);
 
 
-fun domain_type (Type("fun", [T,_])) = T;
+fun domain_type (Type("fun", [T,_])) = T
+and range_type  (Type("fun", [_,T])) = T;
 
 (* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
 fun binder_types (Type("fun",[S,T])) = S :: binder_types T