# HG changeset patch
# User wenzelm
# Date 1320919326 -3600
# Node ID f28329338d30579b34f703d7271365f9d687a8c9
# Parent  4283f3a57cf52f2a3027d05711848628981306eb
simultaneous check;
tight maxidx;

diff -r 4283f3a57cf5 -r f28329338d30 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Nov 09 23:16:47 2011 +0100
+++ b/src/HOL/Tools/record.ML	Thu Nov 10 11:02:06 2011 +0100
@@ -688,8 +688,8 @@
                     val types = map snd fields';
                     val (args, rest) = split_args (map fst fields') fargs
                       handle Fail msg => err msg;
-                    val argtypes = map (Syntax.check_typ ctxt o Syntax_Phases.decode_typ) args;
-                    val varifyT = varifyT (fold Term.maxidx_typ argtypes 0 + 1);
+                    val argtypes = Syntax.check_typs ctxt (map Syntax_Phases.decode_typ args);
+                    val varifyT = varifyT (fold Term.maxidx_typ argtypes ~1 + 1);
                     val vartypes = map varifyT types;
 
                     val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty