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.
Fixed bug in bugfix for function package
authoreberlm
Wed, 28 Jan 2015 14:24:29 +0100
changeset 59455 2bd467b71d15
parent 59454 588b81d19823
child 59456 180555df34ea
Fixed bug in bugfix for function package
src/HOL/Tools/Function/mutual.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Function/mutual.ML	Wed Jan 28 12:26:56 2015 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Wed Jan 28 14:24:29 2015 +0100
@@ -254,6 +254,7 @@
           (fn (i, T) => fn (acc, ctxt) =>
             case mk_var ("x" ^ string_of_int i) T ctxt of (x, ctxt) => (x :: acc, ctxt))
           cargTs ([], name_ctxt)
+    val arg_vars = rev arg_vars
 
     val argsT = fastype_of (HOLogic.mk_tuple arg_vars)
     val (args, name_ctxt) = mk_var "x" argsT name_ctxt
isabelle