From 859a3d35eaada57f0cfd820d71da0beec07ffdc9 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Sat, 13 Feb 2016 14:21:08 -0800
Subject: [PATCH] feat(library/defeq_simplifier): no need to reverse args

---
 src/library/defeq_simplifier.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/library/defeq_simplifier.cpp b/src/library/defeq_simplifier.cpp
index ad611c010..fd30f4f40 100644
--- a/src/library/defeq_simplifier.cpp
+++ b/src/library/defeq_simplifier.cpp
@@ -157,10 +157,10 @@ class defeq_simplify_fn {
     }
 
     expr defeq_simplify_app(expr const & e) {
-        buffer<expr> args;
-        expr f = defeq_simplify(get_app_args(e, args));
-        for (unsigned i = 0; i < args.size(); ++i) args[i] = defeq_simplify(args[i]);
-        return mk_app(f, args);
+        buffer<expr> rev_args;
+        expr f = defeq_simplify(get_app_rev_args(e, rev_args));
+        for (unsigned i = 0; i < rev_args.size(); ++i) rev_args[i] = defeq_simplify(rev_args[i]);
+        return mk_rev_app(f, rev_args);
     }
 
     /* Rewriting */