New syntax function for types
authorpaulson
Sat, 01 Nov 1997 13:02:19 +0100
changeset 4064 9c18a0c9b6f8
parent 4063 0b19014b9155
child 4065 8862fcb5d44a
New syntax function for types
src/Pure/term.ML
--- 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 _   =  [];