maxidx_of_typs replaces max o map maxidx_of_typ

--- a/src/Pure/type.ML	Fri Nov 01 15:35:28 1996 +0100
+++ b/src/Pure/type.ML	Fri Nov 01 15:37:30 1996 +0100
@@ -1056,7 +1056,7 @@
   If freeze then internal TVars are turned into TFrees, else TVars.*)
 fun infer_types (tsig, const_type, types, sorts, used, freeze, Ts, ts) =
   let
-    val maxidx1 = max(map maxidx_of_typ Ts)+1;
+    val maxidx1 = maxidx_of_typs Ts + 1;
     val () = tyinit(maxidx1+1);
     val us = map (attach_types (tsig, const_type, types, sorts, maxidx1)) ts;
     val u = list_comb(Const("",Ts ---> propT),us)