Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simultaneous check;
authorwenzelm
Thu, 10 Nov 2011 11:02:06 +0100
changeset 45434 f28329338d30
parent 45433 4283f3a57cf5
child 45439 34de78f802aa
simultaneous check; tight maxidx;
src/HOL/Tools/record.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle