# HG changeset patch
# User paulson
# Date 846858723 -3600
# Node ID 6854b692f1fe117662ae7b4a296f4ccdd9757b1e
# Parent  5e8db0bc195e9d1d562e33fbdc4c47ee45cd41cb
maxidx_of_typs replaces max o map maxidx_of_typ
Now uses Int.max instead of max

diff -r 5e8db0bc195e -r 6854b692f1fe src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Nov 01 15:30:49 1996 +0100
+++ b/src/Pure/term.ML	Fri Nov 01 15:32:03 1996 +0100
@@ -427,19 +427,20 @@
 
 
 (*Computing the maximum index of a typ*)
-fun maxidx_of_typ(Type(_,Ts)) =
-	if Ts=[] then ~1 else max(map maxidx_of_typ Ts)
+fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts
   | maxidx_of_typ(TFree _) = ~1
-  | maxidx_of_typ(TVar((_,i),_)) = i;
+  | maxidx_of_typ(TVar((_,i),_)) = i
+and maxidx_of_typs [] = ~1
+  | maxidx_of_typs (T::Ts) = Int.max(maxidx_of_typ T, maxidx_of_typs Ts);
 
 
 (*Computing the maximum index of a term*)
 fun maxidx_of_term (Const(_,T)) = maxidx_of_typ T
   | maxidx_of_term (Bound _) = ~1
   | maxidx_of_term (Free(_,T)) = maxidx_of_typ T
-  | maxidx_of_term (Var ((_,i), T)) = max[i, maxidx_of_typ T]
-  | maxidx_of_term (Abs (_,T,body)) = max[maxidx_of_term body, maxidx_of_typ T]
-  | maxidx_of_term (f$t) = max [maxidx_of_term f,  maxidx_of_term t];
+  | maxidx_of_term (Var ((_,i), T)) = Int.max(i, maxidx_of_typ T)
+  | maxidx_of_term (Abs (_,T,u)) = Int.max(maxidx_of_term u, maxidx_of_typ T)
+  | maxidx_of_term (f$t) = Int.max(maxidx_of_term f,  maxidx_of_term t);
 
 
 (* Increment the index of all Poly's in T by k *)