From 1042bbc06faa8da50e27e8d7acf8112c78e58b2d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 2 Mar 2015 13:01:50 -0800
Subject: [PATCH] fix(kernel/metavar): improve error messages by propagating
 the tag when we execute instantiate_all

This is the real fix for commit ededf4fc6c63b0dd21268ca2a10cd982ae52174b
---
 src/kernel/metavar.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index 358b306cf..b898c5717 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -185,7 +185,7 @@ protected:
         if (!modified)
             return e;
         else
-            return mk_rev_app(new_f, new_args);
+            return mk_rev_app(new_f, new_args, e.get_tag());
     }
 
     expr save_result(expr const & e, expr && r) {