# HG changeset patch
# User paulson
# Date 878385739 -3600
# Node ID 9c18a0c9b6f8e7f80c19a4bca3357c1b4638f41d
# Parent  0b19014b9155322b2b929e9bfa65153c19565b11
New syntax function for types

diff -r 0b19014b9155 -r 9c18a0c9b6f8 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 _   =  [];