# HG changeset patch
# User wenzelm
# Date 1291207051 -3600
# Node ID 82baff065334ba9f52e6bf34a722df520b3bdfb1
# Parent  2f97215e79bfb8aec316b14db8981befb1a868e3
tuned;

diff -r 2f97215e79bf -r 82baff065334 src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Dec 01 13:09:08 2010 +0100
+++ b/src/Pure/term.ML	Wed Dec 01 13:37:31 2010 +0100
@@ -284,24 +284,24 @@
   | dest_comb t = raise TERM("dest_comb", [t]);
 
 
-fun domain_type (Type("fun", [T,_])) = T
-and range_type  (Type("fun", [_,T])) = T;
+fun domain_type (Type ("fun", [T, _])) = T;
+
+fun range_type (Type ("fun", [_, U])) = U;
 
 fun dest_funT (Type ("fun", [T, U])) = (T, U)
   | dest_funT T = raise TYPE ("dest_funT", [T], []);
 
 
 (* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
-fun binder_types (Type("fun",[S,T])) = S :: binder_types T
-  | binder_types _   =  [];
+fun binder_types (Type ("fun", [T, U])) = T :: binder_types U
+  | binder_types _ = [];
 
 (* maps  [T1,...,Tn]--->T  to T*)
-fun body_type (Type("fun",[S,T])) = body_type T
-  | body_type T   =  T;
+fun body_type (Type ("fun", [_, U])) = body_type U
+  | body_type T = T;
 
 (* maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T)  *)
-fun strip_type T : typ list * typ =
-  (binder_types T, body_type T);
+fun strip_type T = (binder_types T, body_type T);
 
 
 (*Compute the type of the term, checking that combinations are well-typed
@@ -1007,5 +1007,5 @@
 
 end;
 
-structure BasicTerm: BASIC_TERM = Term;
-open BasicTerm;
+structure Basic_Term: BASIC_TERM = Term;
+open Basic_Term;