From e78173f36b94fa14d8ae434020806dfd5dbdd506 Mon Sep 17 00:00:00 2001
From: Andrei Paskevich <andrei@tertium.org>
Date: Sun, 25 Apr 2010 18:40:48 +0000
Subject: [PATCH] bugfix: actual transformation application was accidentally
 removed

---
 src/transform/eliminate_if.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/transform/eliminate_if.ml b/src/transform/eliminate_if.ml
index bce1a8087..33b721737 100644
--- a/src/transform/eliminate_if.ml
+++ b/src/transform/eliminate_if.ml
@@ -65,7 +65,7 @@ let add_ld axl d = match d with
       let vl,e = open_ls_defn ld in
       begin match e with
         | Term t when has_if t ->
-            let f = ls_defn_axiom ld in
+            let f = elim_f (ls_defn_axiom ld) in
             let nm = ls.ls_name.id_short ^ "_def" in
             let pr = create_prsymbol (id_derive nm ls.ls_name) in
             create_prop_decl Paxiom pr f :: axl, (ls, None)
-- 
GitLab