Commit e78173f3 authored by Andrei Paskevich's avatar Andrei Paskevich

bugfix: actual transformation application was accidentally removed

parent 0e266c78
...@@ -65,7 +65,7 @@ let add_ld axl d = match d with ...@@ -65,7 +65,7 @@ let add_ld axl d = match d with
let vl,e = open_ls_defn ld in let vl,e = open_ls_defn ld in
begin match e with begin match e with
| Term t when has_if t -> | 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 nm = ls.ls_name.id_short ^ "_def" in
let pr = create_prsymbol (id_derive nm ls.ls_name) in let pr = create_prsymbol (id_derive nm ls.ls_name) in
create_prop_decl Paxiom pr f :: axl, (ls, None) create_prop_decl Paxiom pr f :: axl, (ls, None)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment