diff --git a/src/core/decl.ml b/src/core/decl.ml
index 61592ee0d18f62d85205f51895a00c5ba60111b3..478c02cddf3c34565aaf5da8aecf1cfdb177e23e 100644
--- a/src/core/decl.ml
+++ b/src/core/decl.ml
@@ -44,16 +44,15 @@ let check_fvs f =
   Svs.iter (fun vs -> raise (UnboundVar vs)) fvs;
   f
 
-let check_ty ty ty' =
-  if not (ty_equal ty ty') then raise (TypeMismatch (ty,ty'))
+let check_ty = Ty.check_ty_equal
 
 let check_vl ty v = check_ty ty v.vs_ty
-let check_tl ty t = check_ty ty t.t_ty
+let check_tl ty t = check_ty ty (t_type t)
 
 let make_fs_defn fs vl t =
-  let hd = t_app fs (List.map t_var vl) t.t_ty in
+  let hd = e_app fs (List.map t_var vl) t.t_ty in
   let fd = f_forall_close vl [] (f_equ hd t) in
-  check_ty (of_option fs.ls_value) t.t_ty;
+  check_oty_equal fs.ls_value t.t_ty;
   List.iter2 check_vl fs.ls_args vl;
   fs, Some (fs, check_fvs fd)
 
diff --git a/src/core/pattern.ml b/src/core/pattern.ml
index a0d0be9fa9d5153fec791ef2492c0fd77246b6a8..2f2c73d87cfeb3f89f19b7f89dd4171fb19aad23 100644
--- a/src/core/pattern.ml
+++ b/src/core/pattern.ml
@@ -38,12 +38,12 @@ module Compile (X : Action) = struct
 
   let rec compile constructors tl rl = match tl,rl with
     | _, [] -> (* no actions *)
-        let pl = List.map (fun t -> pat_wild t.t_ty) tl in
+        let pl = List.map (fun t -> pat_wild (t_type t)) tl in
         raise (NonExhaustive pl)
     | [], (_,a) :: _ -> (* no terms, at least one action *)
         a
     | t :: tl, _ -> (* process the leftmost column *)
-        let ty = t.t_ty in
+        let ty = t_type t in
         (* extract the set of constructors *)
         let css = match ty.ty_node with
           | Tyapp (ts,_) ->
diff --git a/src/core/pretty.ml b/src/core/pretty.ml
index 2f99549d8d2d8a0c7e704731d3f6b4980d09a806..16ca6d4cafcf8cb842919d9152d9d9baad681804 100644
--- a/src/core/pretty.ml
+++ b/src/core/pretty.ml
@@ -233,7 +233,7 @@ and print_tnode pri fmt t = match t.t_node with
       print_app pri fs fmt tl
   | Tapp (fs, tl) ->
       fprintf fmt (protect_on (pri > 0) "%a:%a")
-        (print_app 5 fs) tl print_ty t.t_ty
+        (print_app 5 fs) tl print_ty (t_type t)
   | Tif (f,t1,t2) ->
       fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
         print_fmla f print_term t1 print_term t2
@@ -494,6 +494,8 @@ let () = Exn_printer.register
       fprintf fmt "Type variable %a is used twice" print_tv tv
   | Ty.UnboundTypeVar tv ->
       fprintf fmt "Unbound type variable: %a" print_tv tv
+  | Ty.UnexpectedProp ->
+      fprintf fmt "Unexpected propositional type"
   | Term.BadArity (ls, ls_arg, app_arg) ->
       fprintf fmt "Bad arity: symbol %a must be applied \
                    to %i arguments, but is applied to %i"
@@ -508,6 +510,10 @@ let () = Exn_printer.register
       fprintf fmt "Not a function symbol: %a" print_ls ls
   | Term.PredicateSymbolExpected ls ->
       fprintf fmt "Not a predicate symbol: %a" print_ls ls
+  | Term.TermExpected t ->
+      fprintf fmt "Not a term: %a" print_term t
+  | Term.FmlaExpected t ->
+      fprintf fmt "Not a formula: %a" print_term t
   | Term.NoMatch ->
       fprintf fmt "Uncatched Term.NoMatch exception: [tf]_match failed"
   | Pattern.ConstructorExpected ls ->
diff --git a/src/core/printer.ml b/src/core/printer.ml
index 1b1d066501cbe82b2f15cda42d9e71404a5ae071..378102cc788b9f4afeadc6d33413b22344e149cd 100644
--- a/src/core/printer.ml
+++ b/src/core/printer.ml
@@ -132,8 +132,8 @@ let syntax_arguments_typed s print_arg print_type t fmt l =
       let grp = String.sub grp 1 (String.length grp - 1) in
       let i = int_of_string grp in
       if i = 0
-      then print_type fmt (Util.of_option t).t_ty
-      else print_type fmt args.(i-1).t_ty
+      then print_type fmt (t_type (Util.of_option t))
+      else print_type fmt (t_type args.(i-1))
     else
       let i = int_of_string grp in
       print_arg fmt args.(i-1) in
diff --git a/src/core/term.ml b/src/core/term.ml
index 92510ed6244b028b65ebb9c0ebc90ef063bfb1a6..fe333be0a5f270f48724fbf7faaf3127fcfef7b5 100644
--- a/src/core/term.ml
+++ b/src/core/term.ml
@@ -178,9 +178,6 @@ let pat_map fn pat = match pat.pat_node with
   | Pas (p, v) -> pat_as (fn p) v
   | Por (p, q) -> pat_or (fn p) (fn q)
 
-let check_ty_equal ty1 ty2 =
-  if not (ty_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))
-
 let protect fn pat =
   let res = fn pat in
   check_ty_equal pat.pat_ty res.pat_ty;
@@ -271,7 +268,7 @@ type term = {
   t_label : label list;
   t_loc   : Loc.position option;
   t_vars  : Svs.t;
-  t_ty    : ty;
+  t_ty    : oty;
   t_tag   : int;
 }
 
@@ -330,6 +327,15 @@ let f_equal : fmla -> fmla -> bool = (==)
 let t_hash t = t.t_tag
 let f_hash f = f.f_tag
 
+(* extract the type of a term *)
+
+exception TermExpected of term
+exception FmlaExpected of term
+
+let t_type t = match t.t_ty with
+  | Some ty -> ty
+  | None -> raise (TermExpected t)
+
 (* expr and trigger equality *)
 
 let e_equal e1 e2 = match e1, e2 with
@@ -400,7 +406,7 @@ module Hsterm = Hashcons.Make (struct
     | _ -> false
 
   let equal t1 t2 =
-    ty_equal t1.t_ty t2.t_ty &&
+    oty_equal t1.t_ty t2.t_ty &&
     t_equal_node t1.t_node t2.t_node &&
     list_all2 (=) t1.t_label t2.t_label
 
@@ -424,7 +430,7 @@ module Hsterm = Hashcons.Make (struct
 
   let hash t =
     Hashcons.combine (t_hash_node t.t_node)
-      (Hashcons.combine_list Hashtbl.hash (ty_hash t.t_ty) t.t_label)
+      (Hashcons.combine_list Hashtbl.hash (oty_hash t.t_ty) t.t_label)
 
   let add_t_vars s t = Svs.union s t.t_vars
   let add_b_vars s (_,b,_) = Svs.union s b.bv_vars
@@ -552,10 +558,10 @@ let mk_term n ty = Hsterm.hashcons {
   t_tag   = -1
 }
 
-let t_var v         = mk_term (Tvar v) v.vs_ty
-let t_const c ty    = mk_term (Tconst c) ty
-let t_int_const s   = mk_term (Tconst (ConstInt s)) Ty.ty_int
-let t_real_const r  = mk_term (Tconst (ConstReal r)) Ty.ty_real
+let t_var v         = mk_term (Tvar v) (Some v.vs_ty)
+let t_const c ty    = mk_term (Tconst c) (Some ty)
+let t_int_const s   = mk_term (Tconst (ConstInt s)) (Some Ty.ty_int)
+let t_real_const r  = mk_term (Tconst (ConstReal r)) (Some Ty.ty_real)
 let t_app f tl ty   = mk_term (Tapp (f, tl)) ty
 let t_if f t1 t2    = mk_term (Tif (f, t1, t2)) t2.t_ty
 let t_let t1 bt ty  = mk_term (Tlet (t1, bt)) ty
@@ -903,16 +909,14 @@ let f_open_quant_cb fq =
 (* constructors with type checking *)
 
 let ls_arg_inst ls tl =
-  let mtch s ty t = ty_match s ty t.t_ty in
+  let mtch s ty t = ty_match s ty (t_type t) in
   try List.fold_left2 mtch Mtv.empty ls.ls_args tl
   with Invalid_argument _ -> raise (BadArity
     (ls, List.length ls.ls_args, List.length tl))
 
 let t_app_infer ls tl =
   let s = ls_arg_inst ls tl in
-  match ls.ls_value with
-    | Some ty -> t_app ls tl (ty_inst s ty)
-    | None -> raise (FunctionSymbolExpected ls)
+  t_app ls tl (oty_inst s ls.ls_value)
 
 let ls_app_inst ls tl ty =
   let s = ls_arg_inst ls tl in
@@ -925,7 +929,8 @@ let ls_app_inst ls tl ty =
 let fs_app_inst fs tl ty = ls_app_inst fs tl (Some ty)
 let ps_app_inst ps tl    = ls_app_inst ps tl (None)
 
-let t_app fs tl ty = ignore (fs_app_inst fs tl ty); t_app fs tl ty
+let e_app ls tl ty = ignore (ls_app_inst ls tl ty); t_app ls tl ty
+let t_app fs tl ty = ignore (fs_app_inst fs tl ty); t_app fs tl (Some ty)
 let f_app ps tl    = ignore (ps_app_inst ps tl);    f_app ps tl
 
 exception EmptyCase
@@ -936,8 +941,8 @@ let t_case t bl =
     | _ -> raise EmptyCase
   in
   let t_check_branch (p,_,tbr) =
-    check_ty_equal p.pat_ty t.t_ty;
-    check_ty_equal ty tbr.t_ty
+    check_ty_equal p.pat_ty (t_type t);
+    check_oty_equal ty tbr.t_ty
   in
   List.iter t_check_branch bl;
   t_case t bl ty
@@ -945,25 +950,25 @@ let t_case t bl =
 let f_case t bl =
   if bl = [] then raise EmptyCase;
   let f_check_branch (p,_,_) =
-    check_ty_equal p.pat_ty t.t_ty
+    check_ty_equal p.pat_ty (t_type t)
   in
   List.iter f_check_branch bl;
   f_case t bl
 
 let t_if f t1 t2 =
-  check_ty_equal t1.t_ty t2.t_ty;
+  check_oty_equal t1.t_ty t2.t_ty;
   t_if f t1 t2
 
 let t_let t1 ((v,_,t2) as bt) =
-  check_ty_equal v.vs_ty t1.t_ty;
+  check_ty_equal v.vs_ty (t_type t1);
   t_let t1 bt t2.t_ty
 
 let f_let t1 ((v,_,_) as bf) =
-  check_ty_equal v.vs_ty t1.t_ty;
+  check_ty_equal v.vs_ty (t_type t1);
   f_let t1 bf
 
 let t_eps ((v,_,_) as bf) =
-  t_eps bf v.vs_ty
+  t_eps bf (Some v.vs_ty)
 
 let t_const c = match c with
   | ConstInt _ -> t_const c ty_int
@@ -1024,7 +1029,7 @@ let fs_tuple = Util.memo_int 17 (fun n ->
 let is_fs_tuple fs = fs == fs_tuple (List.length fs.ls_args)
 
 let t_tuple tl =
-  let ty = ty_tuple (List.map (fun t -> t.t_ty) tl) in
+  let ty = ty_tuple (List.map t_type tl) in
   t_app (fs_tuple (List.length tl)) tl ty
 
 (** Term library *)
@@ -1040,12 +1045,12 @@ let rec t_gen_map fnT fnL m t =
   t_label_copy t (match t.t_node with
     | Tvar v ->
         let r = Mvs.find_default v t m in
-        check_ty_equal (fnT t.t_ty) r.t_ty;
+        check_ty_equal (fnT (t_type t)) (t_type r);
         r
     | Tconst _ ->
         t
     | Tapp (fs, tl) ->
-        t_app (fnL fs) (List.map fn_t tl) (fnT t.t_ty)
+        t_app (fnL fs) (List.map fn_t tl) (fnT (t_type t))
     | Tif (f, t1, t2) ->
         t_if (fn_f f) (fn_t t1) (fn_t t2)
     | Tlet (t1, (u,b,t2)) ->
@@ -1121,7 +1126,7 @@ let f_ty_subst mapT mapV f = f_gen_map (ty_inst mapT) (fun ls -> ls) mapV f
 let rec t_gen_fold fnT fnL acc t =
   let fn_t = t_gen_fold fnT fnL in
   let fn_f = f_gen_fold fnT fnL in
-  let acc = fnT acc t.t_ty in
+  let acc = fnT acc (t_type t) in
   match t.t_node with
   | Tconst _ | Tvar _ -> acc
   | Tapp (f, tl) -> List.fold_left fn_t (fnL acc f) tl
@@ -1177,13 +1182,13 @@ let f_ty_fold fn acc f = f_gen_fold fn Util.const acc f
 let rec t_app_fold fn acc t =
   let acc = t_fold_unsafe (t_app_fold fn) (f_app_fold fn) acc t in
   match t.t_node with
-    | Tapp (ls,tl) -> fn acc ls (List.map (fun t -> t.t_ty) tl) (Some t.t_ty)
+    | Tapp (ls,tl) -> fn acc ls (List.map t_type tl) t.t_ty
     | _ -> acc
 
 and f_app_fold fn acc f =
   let acc = f_fold_unsafe (t_app_fold fn) (f_app_fold fn) acc f in
   match f.f_node with
-    | Fapp (ls,tl) -> fn acc ls (List.map (fun t -> t.t_ty) tl) None
+    | Fapp (ls,tl) -> fn acc ls (List.map t_type tl) None
     | _ -> acc
 
 (* free type variables *)
@@ -1221,7 +1226,7 @@ let f_map fnT fnF f = match f.f_node with
 
 let protect fn t =
   let res = fn t in
-  check_ty_equal t.t_ty res.t_ty;
+  check_oty_equal t.t_ty res.t_ty;
   res
 
 let t_map fnT = t_map (protect fnT)
@@ -1323,7 +1328,7 @@ let f_map_fold fnT fnF acc f = match f.f_node with
 
 let protect_fold fn acc t =
   let acc,res = fn acc t in
-  check_ty_equal t.t_ty res.t_ty;
+  check_oty_equal t.t_ty res.t_ty;
   acc,res
 
 let t_map_fold fnT = t_map_fold (protect_fold fnT)
@@ -1351,7 +1356,7 @@ let t_map_cont fnT fnF contT t =
   match t.t_node with
   | Tvar _ | Tconst _ -> contT t
   | Tapp (fs, tl) ->
-      let cont_app tl = contT (t_app fs tl t.t_ty) in
+      let cont_app tl = contT (e_app fs tl t.t_ty) in
       list_map_cont fnT cont_app tl
   | Tif (f, t1, t2) ->
       let cont_else f t1 t2 = contT (t_if f t1 t2) in
@@ -1415,7 +1420,7 @@ let f_map_cont fnT fnF contF f =
       fnT cont_case t1
 
 let protect_cont t contT e =
-  check_ty_equal t.t_ty e.t_ty;
+  check_oty_equal t.t_ty e.t_ty;
   contT e
 
 let t_map_cont fnT = t_map_cont (fun c t -> fnT (protect_cont t c) t)
@@ -1425,7 +1430,7 @@ let f_map_cont fnT = f_map_cont (fun c t -> fnT (protect_cont t c) t)
 
 let protect_vs fn v =
   let res = fn v in
-  check_ty_equal v.vs_ty res.t_ty;
+  check_ty_equal v.vs_ty (t_type res);
   res
 
 let t_v_map fn t =
@@ -1455,11 +1460,11 @@ let f_occurs_single v f = Svs.mem v f.f_vars
 (* replaces variables with terms in term [t] using map [m] *)
 
 let t_subst m t =
-  Mvs.iter (fun v t -> check_ty_equal v.vs_ty t.t_ty) m;
+  Mvs.iter (fun v t -> check_ty_equal v.vs_ty (t_type t)) m;
   t_subst_unsafe m t
 
 let f_subst m f =
-  Mvs.iter (fun v t -> check_ty_equal v.vs_ty t.t_ty) m;
+  Mvs.iter (fun v t -> check_ty_equal v.vs_ty (t_type t)) m;
   f_subst_unsafe m f
 
 let t_subst_single v t1 t = t_subst (Mvs.singleton v t1) t
@@ -1495,7 +1500,7 @@ let rec pat_equal_alpha p1 p2 =
   | _ -> false
 
 let rec t_equal_alpha c1 c2 m1 m2 t1 t2 =
-  t_equal t1 t2 || ty_equal t1.t_ty t2.t_ty &&
+  t_equal t1 t2 || oty_equal t1.t_ty t2.t_ty &&
   let t_eq = t_equal_alpha c1 c2 m1 m2 in
   let f_eq = f_equal_alpha c1 c2 m1 m2 in
   match t1.t_node, t2.t_node with
@@ -1682,7 +1687,7 @@ exception NoMatch
 
 let rec t_match s t1 t2 =
   if t_equal t1 t2 then s else
-  if not (ty_equal t1.t_ty t2.t_ty) then raise NoMatch else
+  if not (oty_equal t1.t_ty t2.t_ty) then raise NoMatch else
   match t1.t_node, t2.t_node with
     | Tconst c1, Tconst c2 when c1 = c2 -> s
     | Tvar v1, _ ->
@@ -1749,11 +1754,11 @@ and f_subst_term t1 t2 f =
   f_map (t_subst_term t1 t2) (f_subst_term t1 t2) f
 
 let t_subst_term t1 t2 t =
-  check_ty_equal t1.t_ty t2.t_ty;
+  check_oty_equal t1.t_ty t2.t_ty;
   t_subst_term t1 t2 t
 
 let f_subst_term t1 t2 f =
-  check_ty_equal t1.t_ty t2.t_ty;
+  check_oty_equal t1.t_ty t2.t_ty;
   f_subst_term t1 t2 f
 
 (* substitutes fmla [f2] for fmla [f1] in term [t] *)
@@ -1773,11 +1778,11 @@ and f_subst_term_alpha t1 t2 f =
   f_map (t_subst_term_alpha t1 t2) (f_subst_term_alpha t1 t2) f
 
 let t_subst_term_alpha t1 t2 t =
-  check_ty_equal t1.t_ty t2.t_ty;
+  check_oty_equal t1.t_ty t2.t_ty;
   t_subst_term_alpha t1 t2 t
 
 let f_subst_term_alpha t1 t2 f =
-  check_ty_equal t1.t_ty t2.t_ty;
+  check_oty_equal t1.t_ty t2.t_ty;
   f_subst_term_alpha t1 t2 f
 
 (* substitutes fmla [f2] for fmla [f1] in term [t] modulo alpha *)
diff --git a/src/core/term.mli b/src/core/term.mli
index 36d49abf62b3bcdb877ba39465090107c16ad586..4bde7e898d79fb75805c9eaff3c58db2cfde8d25 100644
--- a/src/core/term.mli
+++ b/src/core/term.mli
@@ -45,7 +45,7 @@ val create_vsymbol : preid -> ty -> vsymbol
 type lsymbol = private {
   ls_name   : ident;
   ls_args   : ty list;
-  ls_value  : ty option;
+  ls_value  : oty;
 }
 
 module Mls : Map.S with type key = lsymbol
@@ -57,7 +57,7 @@ val ls_equal : lsymbol -> lsymbol -> bool
   (** equality of function and predicate symbols *)
 val ls_hash : lsymbol -> int
 
-val create_lsymbol : preid -> ty list -> ty option -> lsymbol
+val create_lsymbol : preid -> ty list -> oty -> lsymbol
 val create_fsymbol : preid -> ty list -> ty -> lsymbol
 val create_psymbol : preid -> ty list -> lsymbol
 
@@ -131,7 +131,7 @@ type term = private {
   t_label : label list;
   t_loc   : Loc.position option;
   t_vars  : Svs.t;
-  t_ty    : ty;
+  t_ty    : oty;
   t_tag   : int;
 }
 
@@ -239,10 +239,18 @@ val f_open_quant_cb :
 
 (** compute type instance *)
 
-val ls_app_inst : lsymbol -> term list -> ty option -> ty Mtv.t
+val ls_app_inst : lsymbol -> term list -> oty -> ty Mtv.t
 val fs_app_inst : lsymbol -> term list -> ty -> ty Mtv.t
 val ps_app_inst : lsymbol -> term list -> ty Mtv.t
 
+(* temporary functions for term+fmla fusion *)
+
+exception TermExpected of term
+exception FmlaExpected of term
+
+val e_app : lsymbol -> term list -> oty -> term
+val t_type : term -> ty
+
 (** Smart constructors for term *)
 
 val t_var : vsymbol -> term
@@ -361,11 +369,8 @@ val f_ty_fold : ('a -> ty -> 'a) -> 'a -> fmla -> 'a
 
 (* fold over applications in terms and formulas (but not in patterns!) *)
 
-val t_app_fold :
-  ('a -> lsymbol -> ty list -> ty option -> 'a) -> 'a -> term -> 'a
-
-val f_app_fold :
-  ('a -> lsymbol -> ty list -> ty option -> 'a) -> 'a -> fmla -> 'a
+val t_app_fold : ('a -> lsymbol -> ty list -> oty -> 'a) -> 'a -> term -> 'a
+val f_app_fold : ('a -> lsymbol -> ty list -> oty -> 'a) -> 'a -> fmla -> 'a
 
 (** built-in symbols *)
 
diff --git a/src/core/ty.ml b/src/core/ty.ml
index 8359f68420c33358014b8a309518f65fe63c8397..4b45991a9ed7c798b66330e3805f0ff01881513a 100644
--- a/src/core/ty.ml
+++ b/src/core/ty.ml
@@ -265,3 +265,11 @@ let oty_inst m = Util.option_map (ty_inst m)
 let oty_freevars = Util.option_fold ty_freevars
 let oty_cons = Util.option_fold (fun tl t -> t::tl)
 
+let check_ty_equal ty1 ty2 =
+  if not (ty_equal ty1 ty2) then raise (TypeMismatch (ty1, ty2))
+
+let check_oty_equal o1 o2 = match o1,o2 with
+  | Some ty1, Some ty2 -> check_ty_equal ty1 ty2
+  | None, None -> ()
+  | _ -> raise UnexpectedProp
+
diff --git a/src/core/ty.mli b/src/core/ty.mli
index d083a5b7e03e9356c74676415db53caf019ddfb3..d081a55b66e092a86ac1ebe85f36106e7205197a 100644
--- a/src/core/ty.mli
+++ b/src/core/ty.mli
@@ -142,3 +142,6 @@ val oty_match : ty Mtv.t -> oty -> oty -> ty Mtv.t
 val oty_inst  : ty Mtv.t -> oty -> oty
 val oty_freevars : Stv.t -> oty -> Stv.t
 
+val check_ty_equal : ty -> ty -> unit
+val check_oty_equal : oty -> oty -> unit
+
diff --git a/src/parser/denv.ml b/src/parser/denv.ml
index d4ec2147edf0552f8084a17986a3340e648fe4f5..bfa63be60079c1948a662222acb548fb9198df2b 100644
--- a/src/parser/denv.ml
+++ b/src/parser/denv.ml
@@ -204,7 +204,7 @@ let rec term env t = match t.dt_node with
       t_if (fmla env f) (term env t1) (term env t2)
   | Tlet (e1, id, e2) ->
       let e1 = term env e1 in
-      let v = create_user_vs id e1.t_ty in
+      let v = create_user_vs id (t_type e1) in
       let env = Mstr.add id.id v env in
       let e2 = term env e2 in
       t_let_close v e1 e2
@@ -253,7 +253,7 @@ and fmla env = function
       f_app s (List.map (term env) tl)
   | Flet (e1, id, f2) ->
       let e1 = term env e1 in
-      let v = create_user_vs id e1.t_ty in
+      let v = create_user_vs id (t_type e1) in
       let env = Mstr.add id.id v env in
       let f2 = fmla env f2 in
       f_let_close v e1 f2
@@ -319,7 +319,7 @@ and specialize_pattern_node ~loc htv = function
 let rec specialize_term ~loc htv t =
   let dt =
     { dt_node = specialize_term_node  ~loc htv t.t_node;
-      dt_ty   = specialize_ty         ~loc htv t.t_ty; }
+      dt_ty   = specialize_ty         ~loc htv (t_type t); }
   in
   let add_label l t = { t with dt_node = Tnamed (l, t) } in
   let dt = option_apply dt (fun p -> add_label (Lpos p) dt) t.t_loc in
diff --git a/src/printer/coq.ml b/src/printer/coq.ml
index ea2dc95edad9d39a8471323a92fd29fb8ccf7a2e..34e9cca6a80563e55f0f9c104e0dd738c2b9eaf5 100644
--- a/src/printer/coq.ml
+++ b/src/printer/coq.ml
@@ -241,7 +241,7 @@ and print_tnode opl opr info fmt t = match t.t_node with
           then fprintf fmt "(%a %a)" print_ls fs
             (print_space_list (print_term info)) tl
           else fprintf fmt (protect_on opl "(%a%a:%a)") print_ls fs
-            (print_paren_r (print_term info)) tl (print_ty info) t.t_ty
+            (print_paren_r (print_term info)) tl (print_ty info) (t_type t)
     end
 
 and print_fnode opl opr info fmt f = match f.f_node with
diff --git a/src/printer/why3.ml b/src/printer/why3.ml
index b912b3b889f57a45c71fe3da20f200d443534e63..8f2180acd71a01aef0d340b3d9a2ee7e089dec6d 100644
--- a/src/printer/why3.ml
+++ b/src/printer/why3.ml
@@ -200,7 +200,7 @@ and print_tnode pri fmt t = match t.t_node with
       print_tapp pri fs fmt tl
   | Tapp (fs, tl) ->
       fprintf fmt (protect_on (pri > 0) "%a:%a")
-        (print_tapp 0 fs) tl print_ty t.t_ty
+        (print_tapp 0 fs) tl print_ty (t_type t)
   | Tif (f,t1,t2) ->
       fprintf fmt (protect_on (pri > 0) "if @[%a@] then %a@ else %a")
         print_fmla f print_term t1 print_term t2
diff --git a/src/programs/pgm_pretty.ml b/src/programs/pgm_pretty.ml
index 279e07f1471bf456c3ac0979d48e840bf4c3f53c..e111df4f22cbfe21776fdd84e353ce7a0be5b958 100644
--- a/src/programs/pgm_pretty.ml
+++ b/src/programs/pgm_pretty.ml
@@ -13,7 +13,7 @@ open Pgm_ttree
 let rec print_expr fmt e = match e.expr_desc with
   | Elogic t ->
       fprintf fmt "@[<hov 2><term %a : %a>@]" Pretty.print_term t
-	Pretty.print_ty t.t_ty
+	Pretty.print_ty (t_type t)
   | Elocal v ->
       fprintf fmt "%a" print_pv v
   | Eglobal { ps_kind = PSvar v } ->
diff --git a/src/programs/pgm_typing.ml b/src/programs/pgm_typing.ml
index 79e100a70b8805d2b5904777d380db4b6424a157..3e427bbeaca8ee049437b46a89ad0b4354edbd8a 100644
--- a/src/programs/pgm_typing.ml
+++ b/src/programs/pgm_typing.ml
@@ -834,14 +834,14 @@ let ivariant env (t, ps) =
   let t = iterm env t in
   match ps with
     | None ->
-	if not (Ty.ty_equal ty_int t.t_ty) then
+	if not (Ty.ty_equal ty_int (t_type t)) then
 	  errorm ~loc "variant should have type int";
 	t, ps
-    | Some { ls_args = [t1; _] } when Ty.ty_equal t1 t.t_ty ->
+    | Some { ls_args = [t1; _] } when Ty.ty_equal t1 (t_type t) ->
 	t, ps
     | Some { ls_args = [t1; _] } ->
 	errorm ~loc "@[variant has type %a, but is expected to have type %a@]"
-	  Pretty.print_ty t.t_ty Pretty.print_ty t1
+	  Pretty.print_ty (t_type t) Pretty.print_ty t1
     | _ ->
 	assert false
 
@@ -1218,8 +1218,8 @@ and iletrec gl env dl =
 	  None, t
       | Some (phi, r) ->
 	  let p, e, q = t in
-	  let phi0 = create_ivsymbol (id_fresh "variant") phi.t_ty in
-	  let e_phi = { iexpr_desc = IElogic phi; iexpr_type = phi.t_ty;
+	  let phi0 = create_ivsymbol (id_fresh "variant") (t_type phi) in
+	  let e_phi = { iexpr_desc = IElogic phi; iexpr_type = t_type phi;
 			iexpr_loc = e.iexpr_loc } in
 	  let e = { e with iexpr_desc = IElet (phi0, e_phi, e) } in
 	  Some (phi0, phi, r), (p, e, q)
diff --git a/src/programs/pgm_wp.ml b/src/programs/pgm_wp.ml
index 60badbe563d1abc7280959926626928e7829cc79..9c92208921228fab3ad0e7809613987d8225a29e 100644
--- a/src/programs/pgm_wp.ml
+++ b/src/programs/pgm_wp.ml
@@ -112,7 +112,7 @@ let rec old_label env lab f =
 and old_label_term env lab t = match t.t_node with
   | Tapp (ls, [t]) when ls_equal ls (find_ls ~pure:true env "old") ->
       let t = old_label_term env lab t in (* NECESSARY? *)
-      t_app (find_ls ~pure:true env "at") [t; t_var lab] t.t_ty
+      e_app (find_ls ~pure:true env "at") [t; t_var lab] t.t_ty
   | _ ->
       t_map (old_label_term env lab) (old_label env lab) t
 
@@ -309,7 +309,7 @@ let default_exns_post ef =
   List.map default_exn_post xs
 
 let term_at env lab t =
-  t_app (find_ls ~pure:true env "at") [t; t_var lab] t.t_ty
+  e_app (find_ls ~pure:true env "at") [t; t_var lab] t.t_ty
 
 let wp_expl l f =
   f_label ?loc:f.f_loc (("expl:"^l)::Split_goal.stop_split::f.f_label) f
@@ -576,7 +576,7 @@ let rec t_btop env t = match t.t_node with
       f_equ t (t_True env)
 
 and f_btop env f = match f.f_node with
-  | Fapp (ls, [{t_ty = {ty_node = Tyapp (ts, [])}} as l; r])
+  | Fapp (ls, [{t_ty = Some {ty_node = Tyapp (ts, [])}} as l; r])
   when ls_equal ls ps_equ && ts_equal ts (find_ts ~pure:true env "bool") ->
       f_label_copy f (f_iff_simp (t_btop env l) (t_btop env r))
   | _ -> f_map (fun t -> t) (f_btop env) f
diff --git a/src/transform/abstraction.ml b/src/transform/abstraction.ml
index abf95527fbf81197637408a417736fa62a706e4a..b085c2cedeaf76bb4ec1ce6e2f56733da3d05c3f 100644
--- a/src/transform/abstraction.ml
+++ b/src/transform/abstraction.ml
@@ -35,8 +35,8 @@ let abstraction (keep : lsymbol -> bool) =
         t_map abstract_term abstract_fmla t
     | _ ->
         let (ls, tabs) = try Hterm_alpha.find term_table t with Not_found ->
-          let ls = create_fsymbol (id_fresh "abstr") [] t.t_ty in
-          let tabs = t_app ls [] t.t_ty in
+          let ls = create_lsymbol (id_fresh "abstr") [] t.t_ty in
+          let tabs = e_app ls [] t.t_ty in
           Hterm_alpha.add term_table t (ls, tabs);
           ls, tabs in
         extra_decls := ls :: !extra_decls;
diff --git a/src/transform/eliminate_algebraic.ml b/src/transform/eliminate_algebraic.ml
index c3d92d7ed1adea88ec71c495bc6780e8a7332db8..8a574f46bdf5cba451849cd3b9cc23c5d610f98a 100644
--- a/src/transform/eliminate_algebraic.ml
+++ b/src/transform/eliminate_algebraic.ml
@@ -93,13 +93,13 @@ let rec rewriteT kn state t = match t.t_node with
       in
       let w,m = List.fold_left mk_br (None,Mls.empty) bl in
       let find cs = try Mls.find cs m with Not_found -> of_option w in
-      let ts = match t1.t_ty.ty_node with
-        | Tyapp (ts,_) -> ts
+      let ts = match t1.t_ty with
+        | Some { ty_node = Tyapp (ts,_) } -> ts
         | _ -> Printer.unsupportedTerm t uncompiled
       in
       begin match List.map find (find_constructors kn ts) with
         | [t] -> t
-        | tl  -> t_app (Mts.find ts state.mt_map) (t1::tl) t.t_ty
+        | tl  -> e_app (Mts.find ts state.mt_map) (t1::tl) t.t_ty
       end
   | _ ->
       t_map (rewriteT kn state) (rewriteF kn state Svs.empty true) t
@@ -126,10 +126,10 @@ and rewriteF kn state av sign f = match f.f_node with
       let find cs =
         let vl,e = try Mls.find cs m with Not_found ->
           let var = create_vsymbol (id_fresh "w") in
-          let get_var pj = var (t_app_infer pj [t1]).t_ty in
+          let get_var pj = var (t_type (t_app_infer pj [t1])) in
           List.map get_var (Mls.find cs state.pj_map), of_option w
         in
-        let hd = t_app cs (List.map t_var vl) t1.t_ty in
+        let hd = e_app cs (List.map t_var vl) t1.t_ty in
         match t1.t_node with
         | Tvar v when Svs.mem v av ->
             let hd = f_let_close_simp v hd e in if sign
@@ -140,8 +140,8 @@ and rewriteF kn state av sign f = match f.f_node with
             then f_forall_close_simp vl [] (f_implies_simp hd e)
             else f_exists_close_simp vl [] (f_and_simp     hd e)
       in
-      let ts = match t1.t_ty.ty_node with
-        | Tyapp (ts,_) -> ts
+      let ts = match t1.t_ty with
+        | Some { ty_node = Tyapp (ts,_) } -> ts
         | _ -> Printer.unsupportedFmla f uncompiled
       in
       let op = if sign then f_and_simp else f_or_simp in
@@ -246,11 +246,11 @@ let add_projections (state,task) _ts _ty csl =
     let c = ref 0 in
     let add (pjl,tsk) t =
       let id = id_derive (id ^ (incr c; string_of_int !c)) cs.ls_name in
-      let ls = create_fsymbol id [of_option cs.ls_value] t.t_ty in
+      let ls = create_lsymbol id [of_option cs.ls_value] t.t_ty in
       let tsk = add_decl tsk (create_logic_decl [ls, None]) in
       let id = id_derive (ls.ls_name.id_string ^ "_def") ls.ls_name in
       let pr = create_prsymbol id in
-      let hh = t_app ls [hd] t.t_ty in
+      let hh = e_app ls [hd] t.t_ty in
       let ax = f_forall_close (List.rev vl) [] (f_equ hh t) in
       ls::pjl, add_decl tsk (create_prop_decl Paxiom pr ax)
     in
diff --git a/src/transform/eliminate_definition.ml b/src/transform/eliminate_definition.ml
index 7fe86eecb3746de135267069087186ba73ba6915..b38fc82e9663d35a5971731931eef2225a9046ea 100644
--- a/src/transform/eliminate_definition.ml
+++ b/src/transform/eliminate_definition.ml
@@ -85,7 +85,7 @@ let add_ld func pred axl d = match d with
       let vl,e = open_ls_defn ld in begin match e with
         | Term t when func ->
             let nm = ls.ls_name.id_string ^ "_def" in
-            let hd = t_app ls (List.map t_var vl) t.t_ty in
+            let hd = e_app ls (List.map t_var vl) t.t_ty in
             let ax = f_forall_close vl [] (t_insert hd t) in
             let pr = create_prsymbol (id_derive nm ls.ls_name) in
             create_prop_decl Paxiom pr ax :: axl, (ls, None)
diff --git a/src/transform/eliminate_if.ml b/src/transform/eliminate_if.ml
index 457bae56f57cee50a52e4d489e02ee33f31d0542..0915751745e33341dfefa2fc843c8244c3c16310 100644
--- a/src/transform/eliminate_if.ml
+++ b/src/transform/eliminate_if.ml
@@ -76,7 +76,7 @@ let add_ld axl d = match d with
         | Term t when has_if t ->
             let nm = ls.ls_name.id_string ^ "_def" in
             let pr = create_prsymbol (id_derive nm ls.ls_name) in
-            let hd = t_app ls (List.map t_var vl) t.t_ty in
+            let hd = e_app ls (List.map t_var vl) t.t_ty in
             let f = f_forall_close vl [] (elim_f (f_equ hd t)) in
             create_prop_decl Paxiom pr f :: axl, (ls, None)
         | _ ->
diff --git a/src/transform/encoding_bridge.ml b/src/transform/encoding_bridge.ml
index 74edd7fe77ff99137283fce271cdef08e9109f58..adbbdf1deaad0f1853c495750a263a5636fa293c 100644
--- a/src/transform/encoding_bridge.ml
+++ b/src/transform/encoding_bridge.ml
@@ -130,7 +130,7 @@ let conv_ls tenv ls =
 
 (* Convert the argument of a function use the bridge if needed*)
 let conv_arg tenv t aty =
-  let tty = t.t_ty in
+  let tty = t_type t in
   if ty_equal tty aty then t else
     try
       (* polymorph specials t2tb *)
@@ -168,7 +168,7 @@ let rec rewrite_term tenv vsvar t =
         let tl = List.map (fnT vsvar) tl in
         let p = Hls.find tenv.trans_lsymbol p in
         let tl = List.map2 (conv_arg tenv) tl p.ls_args in
-        conv_res_app tenv p tl t.t_ty
+        conv_res_app tenv p tl (t_type t)
     | Tlet (t1, b) ->
         let u,t2,close = t_open_bound_cb b in
         let t1 = fnT vsvar t1 in
diff --git a/src/transform/encoding_decorate.ml b/src/transform/encoding_decorate.ml
index b04d5624dcf997efea849b9645153649d74453f7..2d67a57dc36c6cbd8d2c94d0d2372a4723239674 100644
--- a/src/transform/encoding_decorate.ml
+++ b/src/transform/encoding_decorate.ml
@@ -33,12 +33,12 @@ let ls_poly_deco =
 
 let rec deco_arg kept tvar t =
   let t = deco_term kept tvar t in
-  if Sty.mem t.t_ty kept then t else
-  let tty = term_of_ty tvar t.t_ty in
-  t_app ls_poly_deco [tty;t] t.t_ty
+  if Sty.mem (t_type t) kept then t else
+  let tty = term_of_ty tvar (t_type t) in
+  e_app ls_poly_deco [tty;t] t.t_ty
 
 and deco_term kept tvar t = match t.t_node with
-  | Tapp (fs,tl) -> t_app fs (List.map (deco_arg kept tvar) tl) t.t_ty
+  | Tapp (fs,tl) -> e_app fs (List.map (deco_arg kept tvar) tl) t.t_ty
   | _ -> t_map (deco_term kept tvar) (deco_fmla kept tvar) t
 
 and deco_fmla kept tvar f = match f.f_node with
diff --git a/src/transform/encoding_distinction.ml b/src/transform/encoding_distinction.ml
index 262b323566c2a931ec5eb3a86666333fec1c6fe0..75d62bd379268f258b761f916ba0ffd5fb0172f8 100644
--- a/src/transform/encoding_distinction.ml
+++ b/src/transform/encoding_distinction.ml
@@ -118,9 +118,9 @@ let rec rewrite_term env tvar vsvar t =
     | Tvar x -> Mvs.find x vsvar
     | Tapp(p,tl) ->
       let tl = List.map (fnT vsvar) tl in
-      let p = find_logic env p (List.map (fun t -> t.t_ty) tl)
-        (Some (ty_inst tvar t.t_ty)) in
-      t_app p tl (ty_inst tvar t.t_ty)
+      let ty = oty_inst tvar t.t_ty in
+      let p = find_logic env p (List.map t_type tl) ty in
+      e_app p tl ty
     | Tif(f, t1, t2) ->
       t_if (fnF vsvar f) (fnT vsvar t1) (fnT vsvar t2)
     | Tlet (t1, b) ->
@@ -142,7 +142,7 @@ and rewrite_fmla env tvar vsvar f =
   match f.f_node with
     | Fapp(p, tl) ->
       let tl = List.map (fnT vsvar) tl in
-      let p = find_logic env p (List.map (fun t -> t.t_ty) tl) None in
+      let p = find_logic env p (List.map t_type tl) None in
       f_app p tl
     | Fquant(q, b) ->
       let vl, tl, f1, cb = f_open_quant_cb b in
@@ -155,7 +155,7 @@ and rewrite_fmla env tvar vsvar f =
       let t1 = fnT vsvar t1 and f2 = fnF vsvar' f2 in
       (* Format.eprintf "u.vs_ty : %a == t1.t_ty : %a@." *)
       (*    Pretty.print_ty u.vs_ty Pretty.print_ty t1.t_ty; *)
-      assert (u.vs_ty == t1.t_ty);
+      Ty.check_ty_equal u.vs_ty (t_type t1);
       f_let t1 (cb u f2)
     | _ -> f_map (fun _ -> assert false) (fnF vsvar) f
 
diff --git a/src/transform/encoding_enumeration.ml b/src/transform/encoding_enumeration.ml
index 690e5f283a8e01c2adee83898a8d0f18c7dbafef..5517fcb3aba5349196f14719e554a2b4ee444e57 100644
--- a/src/transform/encoding_enumeration.ml
+++ b/src/transform/encoding_enumeration.ml
@@ -44,8 +44,8 @@ let add_proj tenv ts =
 let proj tenv t ty = match ty.ty_node with
   | Tyapp (ts,_) when Sts.mem ts tenv.enum ->
       let fs = Hts.find tenv.projs ts in
-      t_app fs [t] t.t_ty
-  | _ when ty_s_any (fun ts -> Sts.mem ts tenv.enum) t.t_ty ->
+      e_app fs [t] t.t_ty
+  | _ when ty_s_any (fun ts -> Sts.mem ts tenv.enum) (t_type t) ->
       Printer.unsupportedType ty "complexe finite type"
   | _ -> t
 
@@ -53,14 +53,14 @@ let proj tenv t = match t.t_node with
   | Tapp (ls,_) ->
       proj tenv t (of_option ls.ls_value)
   | Tvar _ | Tconst _ | Teps _ ->
-      proj tenv t t.t_ty
+      proj tenv t (t_type t)
   | Tif _  | Tcase _  | Tlet _ ->
       t
 
 let rec rewrite_term tenv t = match t.t_node with
   | Tapp (fs,tl) ->
       let pin t = proj tenv (rewrite_term tenv t) in
-      t_app fs (List.map pin tl) t.t_ty
+      e_app fs (List.map pin tl) t.t_ty
   | Tcase _ ->
       Printer.unsupportedTerm t "use eliminate_algebraic"
   | _ -> t_map (rewrite_term tenv) (rewrite_fmla tenv) t
diff --git a/src/transform/encoding_explicit.ml b/src/transform/encoding_explicit.ml
index c809b2722a87d5a65b2fa553c0bd8e7f24a79961..710c4491ecc31dec524bd4fce82293ede53ec8d3 100644
--- a/src/transform/encoding_explicit.ml
+++ b/src/transform/encoding_explicit.ml
@@ -68,8 +68,8 @@ module Transform = struct
   (** translation of terms *)
   let rec term_transform varM t = match t.t_node with
     | Tapp(f, terms) ->
-      let terms = args_transform varM f terms (Some t.t_ty) in
-      t_app (findL f) terms t.t_ty
+      let terms = args_transform varM f terms t.t_ty in
+      e_app (findL f) terms t.t_ty
     | _ -> (* default case : traverse *)
       t_map (term_transform varM) (fmla_transform varM) t
 
diff --git a/src/transform/encoding_guard.ml b/src/transform/encoding_guard.ml
index 7e1820a30338ad21034edce03fe92d2523aa0e38..5e0f7b9f697fd633cb5d8233e95f6fd4aeaf170c 100644
--- a/src/transform/encoding_guard.ml
+++ b/src/transform/encoding_guard.ml
@@ -68,7 +68,7 @@ module Transform = struct
       List.fold_left2 fold acc (ls_selects_of_ts ts) tyl
 
   let type_close_select tvs ts fn f =
-    let fold acc t = extract_tvar acc (app_type t) t.t_ty in
+    let fold acc t = extract_tvar acc (app_type t) (t_type t) in
     let tvm = List.fold_left fold Mtv.empty ts in
     let tvs = Mtv.diff (const3 None) tvs tvm in
     let get_vs tv = create_vsymbol (id_clone tv.tv_name) ty_type in
@@ -114,8 +114,8 @@ module Transform = struct
   let rec term_transform kept varM t =
     match t.t_node with
     | Tapp(f, terms) ->
-      let terms = args_transform kept varM f terms t.t_ty in
-      t_app (findL f) terms t.t_ty
+      let terms = args_transform kept varM f terms (t_type t) in
+      e_app (findL f) terms t.t_ty
     | _ -> (* default case : traverse *)
       t_map (term_transform kept varM) (fmla_transform kept varM) t
 
diff --git a/src/transform/encoding_instantiate.ml b/src/transform/encoding_instantiate.ml
index 216af24efb600a189135c301748e3b445f24f63b..f6577cc135181f17e1d0fa0031697ef4dec30c09 100644
--- a/src/transform/encoding_instantiate.ml
+++ b/src/transform/encoding_instantiate.ml
@@ -287,8 +287,8 @@ let rec rewrite_term menv tvar vsvar t =
     | Tvar x -> Mvs.find x vsvar
     | Tapp(p,tl) ->
       let tl' = List.map (fnT vsvar) tl in
-      let p = find_logic menv tvar p tl (Some t.t_ty) in
-      t_app p tl' (projty_real menv tvar t.t_ty)
+      let p = find_logic menv tvar p tl t.t_ty in
+      t_app p tl' (projty_real menv tvar (t_type t))
     | Tif(f, t1, t2) ->
       t_if (fnF vsvar f) (fnT vsvar t1) (fnT vsvar t2)
     | Tlet (t1, b) -> let u,t2,cb = t_open_bound_cb b in
@@ -325,7 +325,7 @@ and rewrite_fmla menv tvar vsvar f =
       let t1 = fnT vsvar t1 and f2 = fnF vsvar' f2 in
       (* Format.eprintf "u.vs_ty : %a == t1.t_ty : %a@." *)
       (*    Pretty.print_ty u.vs_ty Pretty.print_ty t1.t_ty; *)
-      assert (u.vs_ty == t1.t_ty);
+      check_ty_equal u.vs_ty (t_type t1);
       f_let t1 (cb u f2)
     | _ -> f_map (fun _ -> assert false) (fnF vsvar) f
 
diff --git a/src/transform/inlining.ml b/src/transform/inlining.ml
index fcb563ab85832ed193f1aa10c14b2d1929dbbbc2..47f85b8980391781c696cd1c2fa774d6466903e7 100644
--- a/src/transform/inlining.ml
+++ b/src/transform/inlining.ml
@@ -28,11 +28,11 @@ open Task
 let t_unfold env fs tl ty =
   match Mls.find_option fs env with
   | None ->
-      t_app fs tl ty
+      e_app fs tl ty
   | Some (vl, Term e) ->
-      let add (mt,mv) x y = ty_match mt x.vs_ty y.t_ty, Mvs.add x y mv in
+      let add (mt,mv) x y = ty_match mt x.vs_ty (t_type y), Mvs.add x y mv in
       let (mt,mv) = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vl tl in
-      let mt = ty_match mt e.t_ty ty in
+      let mt = oty_match mt e.t_ty ty in
       t_ty_subst mt mv e
   | _ ->
       assert false
@@ -42,7 +42,7 @@ let f_unfold env ps tl =
   | None ->
       f_app ps tl
   | Some (vs, Fmla e) ->
-      let add (mt,mv) x y = ty_match mt x.vs_ty y.t_ty, Mvs.add x y mv in
+      let add (mt,mv) x y = ty_match mt x.vs_ty (t_type y), Mvs.add x y mv in
       let (mt,mv) = List.fold_left2 add (Ty.Mtv.empty, Mvs.empty) vs tl in
       f_ty_subst mt mv e
   | _ ->
diff --git a/src/transform/libencoding.ml b/src/transform/libencoding.ml
index c9361d1cb348e3ec137b186d004795096790ee70..068c0f2318e799fae157e676cf3ec4ad738b46b3 100644
--- a/src/transform/libencoding.ml
+++ b/src/transform/libencoding.ml
@@ -157,7 +157,7 @@ let rec t_monomorph ty_base kept lsmap consts vmap t =
   t_label_copy t (match t.t_node with
     | Tvar v ->
         Mvs.find v vmap
-    | Tconst _ when Sty.mem t.t_ty kept ->
+    | Tconst _ when Sty.mem (t_type t) kept ->
         t
     | Tconst _ ->
         let ls = ls_of_const ty_base t in
diff --git a/src/transform/lift_epsilon.ml b/src/transform/lift_epsilon.ml
index 892cb60e49cf553e09f5e51daa9e746b4843f70a..014a79826d94e79c5dade432c476fa78d58352a6 100644
--- a/src/transform/lift_epsilon.ml
+++ b/src/transform/lift_epsilon.ml
@@ -40,7 +40,7 @@ let lift kind =
         let acc = add_decl acc (Decl.create_logic_decl [xl,None]) in
         let axs =
           Decl.create_prsymbol (Ident.id_derive ("epsilon_def") x.vs_name) in
-        let xlapp = t_app xl (List.map (fun x -> t_var x) fv) t.t_ty in
+        let xlapp = e_app xl (List.map t_var fv) t.t_ty in
         let f =
           match kind with
           (* assume that lambdas always exist *)