diff --git a/src/coq-plugin/whytac.ml b/src/coq-plugin/whytac.ml
index 2560766e6cc2351f5764c3c736ba08944a70f92c..23f6ee0f2a9a031558d8d272c9cf3599002631bd 100644
--- a/src/coq-plugin/whytac.ml
+++ b/src/coq-plugin/whytac.ml
@@ -373,7 +373,7 @@ and tr_global_ts dep env r =
 	      let (_,vars), env, t = decomp_type_quantifiers env ty in
 	      let tvm =
 		let add v1 v2 tvm = 
-		  Idmap.add (id_of_string v1.tv_name.Ident.id_short) v2 tvm
+		  Idmap.add (id_of_string v1.tv_name.Ident.id_string) v2 tvm
 		in
 		List.fold_right2 add vars ts.Ty.ts_args Idmap.empty
 	      in
diff --git a/src/core/env.ml b/src/core/env.ml
index fb81311f31054787fc45fca9b64ffe7d61cc2f1d..e170bb6e8f0167e700ce54e4ede88beb0240dcbf 100644
--- a/src/core/env.ml
+++ b/src/core/env.ml
@@ -40,7 +40,7 @@ let create_env =
       env_tag      = !r }
     in
     let th = builtin_theory in
-    let m = Mnm.add th.th_name.id_short th Mnm.empty in
+    let m = Mnm.add th.th_name.id_string th Mnm.empty in
     Hashtbl.add env.env_memo [] m;
     env
 
diff --git a/src/core/ident.ml b/src/core/ident.ml
index 67312e0a9b0e80af0e89b5a0487b7c0ed0bff546..c44582a27c9f571816b2ed37180ec326f5f8d131 100644
--- a/src/core/ident.ml
+++ b/src/core/ident.ml
@@ -22,10 +22,9 @@ open Util
 (** Identifiers *)
 
 type ident = {
-  id_short : string;    (* non-unique name for string-based lookup *)
-  id_long : string;     (* non-unique name for pretty printing *)
+  id_string : string;   (* non-unique name *)
   id_origin : origin;   (* origin of the ident *)
-  id_tag : int;         (* unique numeric tag *)
+  id_tag    : int;      (* unique numeric tag *)
 }
 
 and origin =
@@ -52,23 +51,16 @@ let gentag = let r = ref 0 in fun () -> incr r; !r
 
 let id_register id = { id with id_tag = gentag () }
 
-let create_ident short long origin = {
-  id_short  = short;
-  id_long   = long;
+let create_ident name origin = {
+  id_string = name;
   id_origin = origin;
   id_tag    = -1
 }
 
-let id_fresh sh = create_ident sh sh Fresh
-let id_fresh_long sh ln = create_ident sh ln Fresh
-
-let id_user sh loc = create_ident sh sh (User loc)
-let id_user_long sh ln loc = create_ident sh ln (User loc)
-
-let id_derive sh id = create_ident sh sh (Derived id)
-let id_derive_long sh ln id = create_ident sh ln (Derived id)
-
-let id_clone id = create_ident id.id_short id.id_long (Derived id)
+let id_fresh nm = create_ident nm Fresh
+let id_user nm loc = create_ident nm (User loc)
+let id_derive nm id = create_ident nm (Derived id)
+let id_clone id = create_ident id.id_string (Derived id)
 let id_dup id = { id with id_tag = -1 }
 
 let rec id_derived_from i1 i2 = id_equal i1 i2 ||
@@ -121,7 +113,7 @@ let id_unique printer ?(sanitizer = same) id =
   try
     Hashtbl.find printer.values id.id_tag
   with Not_found ->
-    let name = sanitizer (printer.sanitizer id.id_long) in
+    let name = sanitizer (printer.sanitizer id.id_string) in
     let name = find_unique printer.indices name in
     Hashtbl.replace printer.values id.id_tag name;
     name
diff --git a/src/core/ident.mli b/src/core/ident.mli
index a35ef3f1cf7995be300533e5fe4321a5edd1f056..ac61943b0bae7f40cfae3be18ecb3c201fde98f2 100644
--- a/src/core/ident.mli
+++ b/src/core/ident.mli
@@ -20,10 +20,9 @@
 (** Identifiers *)
 
 type ident = private {
-  id_short : string;    (* non-unique name for string-based lookup *)
-  id_long : string;     (* non-unique name for pretty printing *)
+  id_string : string;   (* non-unique name *)
   id_origin : origin;   (* origin of the ident *)
-  id_tag : int;         (* unique numeric tag *)
+  id_tag    : int;      (* unique numeric tag *)
 }
 
 and origin =
@@ -45,15 +44,12 @@ val id_register : preid -> ident
 
 (* create a fresh pre-ident *)
 val id_fresh : string -> preid
-val id_fresh_long : string -> string -> preid
 
 (* create a localized pre-ident *)
 val id_user : string -> Loc.position -> preid
-val id_user_long : string -> string -> Loc.position -> preid
 
 (* create a derived pre-ident *)
 val id_derive : string -> ident -> preid
-val id_derive_long : string -> string -> ident -> preid
 
 (* create a derived pre-ident with the same name *)
 val id_clone : ident -> preid
diff --git a/src/core/pretty.ml b/src/core/pretty.ml
index fb280b66403a09ab7fc64d5def09bcbe8d33082c..a9dc50408cc128dba3e0510aef44bf1a80b1a2d8 100644
--- a/src/core/pretty.ml
+++ b/src/core/pretty.ml
@@ -330,7 +330,7 @@ let print_inst fmt (id1,id2) =
     let n = id_unique pprinter id1 in
     fprintf fmt "prop %s = %a" n print_pr (Hid.find phash id2)
   else
-    fprintf fmt "ident %s = %s" id1.id_long id2.id_long
+    fprintf fmt "ident %s = %s" id1.id_string id2.id_string
 
 let print_decl fmt d = match d.d_node with
   | Dtype tl  -> print_list newline print_type_decl fmt tl
diff --git a/src/core/theory.ml b/src/core/theory.ml
index a6410e69b6df5b8f8a0f487fd7c1c5fa08e52c33..2750777d1ba502df5f40d9650cfdfac82132eded 100644
--- a/src/core/theory.ml
+++ b/src/core/theory.ml
@@ -115,10 +115,10 @@ let builtin_theory =
   let kn_equ  = known_add_decl kn_real decl_equ in
   let kn_neq  = known_add_decl kn_equ decl_neq in
 
-  let ns_int  = Mnm.add ts_int.ts_name.id_short ts_int Mnm.empty in
-  let ns_real = Mnm.add ts_real.ts_name.id_short ts_real ns_int in
-  let ns_equ  = Mnm.add ps_equ.ls_name.id_short ps_equ Mnm.empty in
-  let ns_neq  = Mnm.add ps_neq.ls_name.id_short ps_neq ns_equ in
+  let ns_int  = Mnm.add ts_int.ts_name.id_string ts_int Mnm.empty in
+  let ns_real = Mnm.add ts_real.ts_name.id_string ts_real ns_int in
+  let ns_equ  = Mnm.add ps_equ.ls_name.id_string ps_equ Mnm.empty in
+  let ns_neq  = Mnm.add ps_neq.ls_name.id_string ps_neq ns_equ in
 
   let export  = { ns_ts = ns_real;   ns_ls = ns_neq;
                   ns_pr = Mnm.empty; ns_ns = Mnm.empty } in
@@ -215,8 +215,8 @@ let create_theory n = use_export (empty_theory n) builtin_theory
 let add_symbol add id v uc =
   match uc.uc_import, uc.uc_export with
   | i0 :: sti, e0 :: ste -> { uc with
-      uc_import = add false id.id_short v i0 :: sti;
-      uc_export = add true  id.id_short v e0 :: ste;
+      uc_import = add false id.id_string v i0 :: sti;
+      uc_export = add true  id.id_string v e0 :: ste;
       uc_local  = Sid.add id uc.uc_local }
   | _ ->
       assert false
diff --git a/src/driver/driver.ml b/src/driver/driver.ml
index c72cec0596d6e30c4e68646b1a3d846935da60c4..64c0596a15a615ac2657970694096bbdf8602b3b 100644
--- a/src/driver/driver.ml
+++ b/src/driver/driver.ml
@@ -375,7 +375,7 @@ let get_filename drv input_file theory_name goal_name =
   Str.global_substitute filename_regexp replace file
 
 let file_of_task drv input_file theory_name task =
-  get_filename drv input_file theory_name (task_goal task).pr_name.id_short
+  get_filename drv input_file theory_name (task_goal task).pr_name.id_string
 
 let call_on_buffer ?debug ~command ?timelimit ?memlimit drv buffer =
   let regexps = drv.drv_regexps in
diff --git a/src/ide/ide_main.ml b/src/ide/ide_main.ml
index 6e114c810e624216441042ac91163b2f7ac56f6a..1fb9a7f101bb0e67dfbcd52d774a172aede04b98 100644
--- a/src/ide/ide_main.ml
+++ b/src/ide/ide_main.ml
@@ -118,7 +118,7 @@ module Ide_namespace = struct
       Mnm.iter add_ns ns.ns_ns
     in
     let row = model#append () in
-    model#set ~row ~column (th.th_name.Ident.id_short : string);
+    model#set ~row ~column (th.th_name.Ident.id_string : string);
     fill row th.th_export
 
 end
diff --git a/src/main.ml b/src/main.ml
index 62b97c42f492020c725a72a06bab2fee84d14c97..bde1dbb3e85ac3bd0ffd5f5896bb207123b74a82 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -249,7 +249,7 @@ let rec report fmt = function
   | Typing.Error e ->
       Typing.report fmt e
   | Decl.UnknownIdent i ->
-      fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_short
+      fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_string
   | Driver.Error e ->
       Driver.report fmt e
   | Config.Dynlink.Error e ->
@@ -263,7 +263,7 @@ let rec report fmt = function
   | e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
 
 let print_th_namespace fmt th =
-  Pretty.print_namespace fmt th.th_name.Ident.id_short th.th_export
+  Pretty.print_namespace fmt th.th_name.Ident.id_string th.th_export
 
 let fname_printer = ref (Ident.create_ident_printer [])
 
@@ -274,7 +274,7 @@ let do_task _env drv fname tname (th : Why.Theory.theory) (task : Task.task) =
           Prover.prove_task ~debug ~command ~timelimit ~memlimit drv task ()
         in
         printf "%s %s %s : %a@." fname tname
-          (task_goal task).Decl.pr_name.Ident.id_long
+          (task_goal task).Decl.pr_name.Ident.id_string
           Call_provers.print_prover_result res
     | None, None ->
         Prover.print_task ~debug drv std_formatter task
@@ -283,7 +283,7 @@ let do_task _env drv fname tname (th : Why.Theory.theory) (task : Task.task) =
         let fname =
           try Filename.chop_extension fname with _ -> fname
         in
-        let tname = th.th_name.Ident.id_short in
+        let tname = th.th_name.Ident.id_string in
         let dest = Driver.file_of_task drv fname tname task in
         (* Uniquify the filename before the extension if it exists*)
         let i = try String.rindex dest '.' with _ -> String.length dest in
diff --git a/src/manager/test.ml b/src/manager/test.ml
index 6fda69f6a0cf7be99d8b2de509909363d1c33a5c..5ebb42a8f2698cc1fca1834772450cfa6695dbfc 100644
--- a/src/manager/test.ml
+++ b/src/manager/test.ml
@@ -121,7 +121,7 @@ let rec report fmt = function
   | Typing.Error e ->
       Typing.report fmt e
   | Decl.UnknownIdent i ->
-      fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_short
+      fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_string
   | Driver.Error e ->
       Driver.report fmt e
   | Config.Dynlink.Error e ->
@@ -146,7 +146,7 @@ let m : Why.Theory.theory Why.Theory.Mnm.t =
 (***************************)
 
 let add_task (tname : string) (task : Why.Task.task) acc =
-  let name = (Why.Task.task_goal task).Why.Decl.pr_name.Why.Ident.id_long in
+  let name = (Why.Task.task_goal task).Why.Decl.pr_name.Why.Ident.id_string in
   eprintf "doing task: tname=%s, name=%s@." tname name;
   Db.add_or_replace_task ~tname ~name task :: acc
 
@@ -231,11 +231,11 @@ let main_loop goals =
 let () =
   eprintf "looking for goals@.";
   let add_th t th mi = 
-    eprintf "adding theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_long t;
+    eprintf "adding theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_string t;
     Why.Ident.Mid.add th.Why.Theory.th_name (t,th) mi 
   in
   let do_th _ (t,th) glist = 
-    eprintf "doing theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_long t;
+    eprintf "doing theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_string t;
     do_theory t th glist  
   in
   let goals = 
diff --git a/src/parser/denv.ml b/src/parser/denv.ml
index 50ffebecaaf659536fcb1d63d571d028795930db..73dc624ec39f578ca2f746478cb63315ee247f3c 100644
--- a/src/parser/denv.ml
+++ b/src/parser/denv.ml
@@ -58,14 +58,14 @@ let rec print_dty fmt = function
   | Tyvar { type_val = Some t } ->
       print_dty fmt t
   | Tyvar { type_val = None; tvsymbol = v } ->
-      fprintf fmt "'%s" v.tv_name.id_short
+      fprintf fmt "'%s" v.tv_name.id_string
   | Tyapp (s, []) ->
-      fprintf fmt "%s" s.ts_name.id_short
+      fprintf fmt "%s" s.ts_name.id_string
   | Tyapp (s, [t]) -> 
-      fprintf fmt "%a %s" print_dty t s.ts_name.id_short
+      fprintf fmt "%a %s" print_dty t s.ts_name.id_string
   | Tyapp (s, l) -> 
       fprintf fmt "(%a) %s" 
-	(print_list comma print_dty) l s.ts_name.id_short
+	(print_list comma print_dty) l s.ts_name.id_string
 
 let create_ty_decl_var =
   let t = ref 0 in
diff --git a/src/parser/typing.ml b/src/parser/typing.ml
index 2fe1f9438006fcac4eaed903d0140d73aa09b2c7..86c5070a5b78b9ee017a4f53ab8794bad988cf5e 100644
--- a/src/parser/typing.ml
+++ b/src/parser/typing.ml
@@ -87,7 +87,7 @@ let report fmt = function
   | TermExpected ->
       fprintf fmt "syntax error: term expected"
   | BadNumberOfArguments (s, n, m) ->
-      fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_short n;
+      fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_string n;
       fprintf fmt "but is expecting %d arguments@]" m
   | ClashTheory s ->
       fprintf fmt "clash with previous theory %s" s
@@ -709,7 +709,7 @@ let add_types dl th =
 	  let vars = th'.utyvars in
 	  List.iter
 	    (fun v ->
-	       Hashtbl.add vars v.tv_name.id_short
+	       Hashtbl.add vars v.tv_name.id_string
                   (create_ty_decl_var ~user:true v))
 	    ts.ts_args;
 	  ts, th'
@@ -733,7 +733,7 @@ let add_types dl th =
   with ClashSymbol s -> error ~loc:(Hashtbl.find csymbols s) (Clash s)
 
 let env_of_vsymbol_list vl =
-  List.fold_left (fun env v -> Mstr.add v.vs_name.id_short v env) Mstr.empty vl
+  List.fold_left (fun env v -> Mstr.add v.vs_name.id_string v env) Mstr.empty vl
 
 let add_logics dl th =
   let fsymbols = Hashtbl.create 17 in
@@ -931,30 +931,30 @@ and add_decl env lenv th = function
                   let ts1 = find_tysymbol_ns p t.th_export in
                   let ts2 = find_tysymbol q th in
                   if Mts.mem ts1 s.inst_ts
-                  then error ~loc (Clash ts1.ts_name.id_short);
+                  then error ~loc (Clash ts1.ts_name.id_string);
                   { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
               | CSlsym (p,q) ->
                   let ls1 = find_lsymbol_ns p t.th_export in
                   let ls2 = find_lsymbol q th in
                   if Mls.mem ls1 s.inst_ls
-                  then error ~loc (Clash ls1.ls_name.id_short);
+                  then error ~loc (Clash ls1.ls_name.id_string);
                   { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
               | CSlemma p ->
                   let pr,_ = find_prop_ns p t.th_export in
                   if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
-                  then error ~loc (Clash pr.pr_name.id_short);
+                  then error ~loc (Clash pr.pr_name.id_string);
                   { s with inst_lemma = Spr.add pr s.inst_lemma }
               | CSgoal p ->
                   let pr,_ = find_prop_ns p t.th_export in
                   if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
-                  then error ~loc (Clash pr.pr_name.id_short);
+                  then error ~loc (Clash pr.pr_name.id_string);
                   { s with inst_goal = Spr.add pr s.inst_goal }
 	    in
             let s = List.fold_left add_inst empty_inst s in
 	    clone_export th t s
       in
       let n = match use.use_as with
-	| None -> Some t.th_name.id_short
+	| None -> Some t.th_name.id_string
 	| Some (Some x) -> Some x.id
 	| Some None -> None
       in
@@ -982,7 +982,7 @@ and add_decl env lenv th = function
 
 and type_and_add_theory env lenv pt =
   let id = pt.pt_name in
-  if Mnm.mem id.id lenv || id.id = builtin_theory.th_name.id_short
+  if Mnm.mem id.id lenv || id.id = builtin_theory.th_name.id_string
     then error (ClashTheory id.id);
   let th = type_theory env lenv id pt in
   Mnm.add id.id th lenv
diff --git a/src/programs/pgm_typing.ml b/src/programs/pgm_typing.ml
index 0786041b0e912adb5e14c387d3f42d7423695c6b..9ae267e50ed9713106771f75396882b91658e3cc 100644
--- a/src/programs/pgm_typing.ml
+++ b/src/programs/pgm_typing.ml
@@ -483,7 +483,7 @@ let add_decl uc ls =
       | User loc -> Some loc
       | _ -> None (* FIXME: loc for recursive functions *)
     in
-    errorm ?loc "clash with previous symbol %s" ls.ls_name.id_short
+    errorm ?loc "clash with previous symbol %s" ls.ls_name.id_string
     
 let file env uc dl =
   let uc, dl =
@@ -503,7 +503,7 @@ let file env uc dl =
 	     let _, dl = letrec uc Mstr.empty dl in
 	     let one uc (v,_,_,_ as r) =
 	       let tyl, ty = uncurrying uc v.vs_ty in
-	       let id = id_fresh v.vs_name.id_short in
+	       let id = id_fresh v.vs_name.id_string in
 	       let ls = create_lsymbol id tyl (Some ty) in
 	       add_decl uc ls, (ls, r)
 	     in
diff --git a/src/transform/eliminate_algebraic.ml b/src/transform/eliminate_algebraic.ml
index fbc70c3545d6400c76ce89887411a07848af9219..7a33d7094ca18e934ada071856e0c18f1c64514a 100644
--- a/src/transform/eliminate_algebraic.ml
+++ b/src/transform/eliminate_algebraic.ml
@@ -158,7 +158,7 @@ let add_type (state, task) ts csl =
   let cs_add tsk cs = add_decl tsk (create_logic_decl [cs, None]) in
   let task = List.fold_left cs_add task csl in
   (* declare the selector function *)
-  let mt_id = id_derive ("match_" ^ ts.ts_name.id_long) ts.ts_name in
+  let mt_id = id_derive ("match_" ^ ts.ts_name.id_string) ts.ts_name in
   let mt_hd = ty_app ts (List.map ty_var ts.ts_args) in
   let mt_ty = ty_var (create_tvsymbol (id_fresh "a")) in
   let mt_al = mt_hd :: List.rev_map (fun _ -> mt_ty) csl in
@@ -170,7 +170,7 @@ let add_type (state, task) ts csl =
   let mt_vl = List.rev_map mt_vs csl in
   let mt_tl = List.rev_map t_var mt_vl in
   let mt_add tsk cs t =
-    let id = mt_ls.ls_name.id_long ^ "_" ^ cs.ls_name.id_long in
+    let id = mt_ls.ls_name.id_string ^ "_" ^ cs.ls_name.id_string in
     let pr = create_prsymbol (id_derive id cs.ls_name) in
     let vl = List.rev_map (create_vsymbol (id_fresh "u")) cs.ls_args in
     let hd = t_app cs (List.rev_map t_var vl) (of_option cs.ls_value) in
@@ -182,7 +182,7 @@ let add_type (state, task) ts csl =
   let task = List.fold_left2 mt_add task csl mt_tl in
   (* declare and define the projection functions *)
   let pj_add (m,tsk) cs =
-    let id = cs.ls_name.id_long ^ "_proj_" in
+    let id = cs.ls_name.id_string ^ "_proj_" in
     let vl = List.rev_map (create_vsymbol (id_fresh "u")) cs.ls_args in
     let tl = List.rev_map t_var vl in
     let hd = t_app cs tl (of_option cs.ls_value) in
@@ -191,7 +191,7 @@ let add_type (state, task) ts csl =
       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 tsk = add_decl tsk (create_logic_decl [ls, None]) in
-      let id = id_derive (ls.ls_name.id_long ^ "_def") ls.ls_name 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 ax = f_forall (List.rev vl) [[Term hd]] (f_equ hh t) in
@@ -202,7 +202,7 @@ let add_type (state, task) ts csl =
   in
   let pjmap, task = List.fold_left pj_add (state.pj_map, task) csl in
   (* add the inversion axiom *)
-  let ax_id = ts.ts_name.id_long ^ "_inversion" in
+  let ax_id = ts.ts_name.id_string ^ "_inversion" in
   let ax_pr = create_prsymbol (id_derive ax_id ts.ts_name) in
   let ax_vs = create_vsymbol (id_fresh "u") mt_hd in
   let ax_hd = t_var ax_vs in
diff --git a/src/transform/eliminate_definition.ml b/src/transform/eliminate_definition.ml
index 381b53c7a3557ad749b03391ca26391f27055220..bc21991830da642618a1e54fee66ccc3faf8f819 100644
--- a/src/transform/eliminate_definition.ml
+++ b/src/transform/eliminate_definition.ml
@@ -74,13 +74,13 @@ let add_ld func pred axl d = match d with
   | ls, Some ld ->
       let vl,e = open_ls_defn ld in begin match e with
         | Term t when func ->
-            let nm = ls.ls_name.id_short ^ "_def" in
+            let nm = ls.ls_name.id_string ^ "_def" in
             let hd = t_app ls (List.map t_var vl) t.t_ty in
             let ax = f_forall vl [[Term hd]] (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)
         | Fmla f when pred ->
-            let nm = ls.ls_name.id_short ^ "_def" in
+            let nm = ls.ls_name.id_string ^ "_def" in
             let hd = f_app ls (List.map t_var vl) in
             let ax = f_forall vl [[Fmla hd]] (f_insert hd f) in
             let pr = create_prsymbol (id_derive nm ls.ls_name) in
diff --git a/src/transform/eliminate_if.ml b/src/transform/eliminate_if.ml
index 520e8c9fbb15993e2fa7ff92f97f37fa06bb26c1..341d6c954a06cd495dfb994034ec9b793e44fbb3 100644
--- a/src/transform/eliminate_if.ml
+++ b/src/transform/eliminate_if.ml
@@ -69,7 +69,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 nm = ls.ls_name.id_short ^ "_def" in
+            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 f = f_forall vl [[Term hd]] (elim_f (f_equ hd t)) in
diff --git a/src/transform/eliminate_inductive.ml b/src/transform/eliminate_inductive.ml
index 4a78d1a0245ec9eab66ab7991134332a8708bec3..6c0eddb317c72f1231633f1478d57ffb236f6a52 100644
--- a/src/transform/eliminate_inductive.ml
+++ b/src/transform/eliminate_inductive.ml
@@ -46,7 +46,7 @@ let inv acc (ps,al) =
   let hd = f_app ps tl in
   let dj = Util.map_join_left (exi tl) f_or al in
   let ax = f_forall vl [[Fmla hd]] (f_implies hd dj) in
-  let nm = id_derive (ps.ls_name.id_long ^ "_inversion") ps.ls_name in
+  let nm = id_derive (ps.ls_name.id_string ^ "_inversion") ps.ls_name in
   create_prop_decl Paxiom (create_prsymbol nm) ax :: acc
 
 let elim d = match d.d_node with
diff --git a/src/transform/encoding_decorate.ml b/src/transform/encoding_decorate.ml
index ec7656b130b9e051e789e4e333c9a577456ac2aa..401ecee70a57ed562299f611e4bc90e7ce4f4961 100644
--- a/src/transform/encoding_decorate.ml
+++ b/src/transform/encoding_decorate.ml
@@ -41,7 +41,7 @@ struct
 
      
 (*  let spec_conv ts =
-    let name = ts.ts_name.id_short in
+    let name = ts.ts_name.id_string in
     let d2ty = create_fsymbol (id_fresh ("d2"^name)) [deco] (ty_app ts []) in
     let ty2u = create_fsymbol (id_fresh (name^"2u")) [(ty_app ts [])] undeco in
     let axiom = 
@@ -85,7 +85,7 @@ let load_prelude query env =
   let logic_tty = Theory.ns_find_ls builtin.th_export ["tty"] in
   let clone_builtin ts =
     let task = None in
-    let name = ts.ts_name.id_short in
+    let name = ts.ts_name.id_string in
     let th_uc = create_theory (id_fresh ("encoding_decorate_for_"^name)) in
     let th_uc = Theory.use_export th_uc prelude in
     let th_uc = 
@@ -140,7 +140,7 @@ let rec term_of_ty tenv tvar ty =
     | Tyvar tv -> 
         t_var (try Htv.find tvar tv
               with Not_found -> 
-                (let var = create_vsymbol (id_fresh ("tv"^tv.tv_name.id_short))
+                (let var = create_vsymbol (id_fresh ("tv"^tv.tv_name.id_string))
                   tenv.ty in
                  Htv.add tvar tv var;
                  var))