# HG changeset patch
# User paulson
# Date 846859050 -3600
# Node ID 7ef2987da18f3a2231dee7c7a7f74029e304182d
# Parent  0698ddfbf6e498ecd505f0a791d47a3266e0c849
maxidx_of_typs replaces max o map maxidx_of_typ

diff -r 0698ddfbf6e4 -r 7ef2987da18f src/Pure/type.ML
--- 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)