author | paulson |
Sat, 01 Nov 1997 13:02:19 +0100 | |
changeset 4064 | 9c18a0c9b6f8 |
parent 4063 | 0b19014b9155 |
child 4065 | 8862fcb5d44a |
src/Pure/term.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/term.ML Sat Nov 01 13:01:57 1997 +0100 +++ b/src/Pure/term.ML Sat Nov 01 13:02:19 1997 +0100 @@ -98,6 +98,8 @@ | dest_Var t = raise TERM("dest_Var", [t]); +fun domain_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 | binder_types _ = [];