From 6acf7afa16f1ca2886737569a192d6d8fc7defc8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 22 Oct 2015 17:06:48 -0700
Subject: [PATCH] fix(library/type_inference): bug when using apply_beta

---
 src/library/type_inference.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/library/type_inference.cpp b/src/library/type_inference.cpp
index a714ffdd8..639c13cb4 100644
--- a/src/library/type_inference.cpp
+++ b/src/library/type_inference.cpp
@@ -287,7 +287,7 @@ bool type_inference::is_def_eq(levels const & ls1, levels const & ls2) {
     ?m is an assigned mvar, substitute \c ?m with its assignment. */
 expr type_inference::subst_mvar(expr const & e) {
     buffer<expr> args;
-    expr const & m   = get_app_args(e, args);
+    expr const & m   = get_app_rev_args(e, args);
     lean_assert(is_mvar(m));
     expr const * v = get_assignment(m);
     lean_assert(v);