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