From 5cba7244ce8b03dbdf0c9f0ab587e7fa3c188933 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Oct 2014 15:16:38 -0700
Subject: [PATCH] fix(library/tactic/expr_to_tactic): argument evaluation order
 is not part of the standard

---
 src/library/tactic/expr_to_tactic.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp
index d8181eeb9..020175759 100644
--- a/src/library/tactic/expr_to_tactic.cpp
+++ b/src/library/tactic/expr_to_tactic.cpp
@@ -246,8 +246,9 @@ void register_bin_tac(name const & n, std::function<tactic(tactic const &, tacti
             get_app_args(e, args);
             if (args.size() != 2)
                 throw expr_to_tactic_exception(e, "invalid binary tactic, it must have two arguments");
-            return f(expr_to_tactic(tc, fn, args[0], p),
-                     expr_to_tactic(tc, fn, args[1], p));
+            tactic t1 = expr_to_tactic(tc, fn, args[0], p);
+            tactic t2 = expr_to_tactic(tc, fn, args[1], p);
+            return f(t1, t2);
         });
 }