diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index 61a8efc1d40683811146fb60bdf043df6bbaceac..9587d9eac5de4175c7f3de5b56c764c3d86d818e 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -149,8 +149,8 @@ struct
                     [ (Trigger.of_term value1 :: triggers );
                       (Trigger.of_term value2 :: triggers ) ]
                 in
-                let l_name = Pretty_utils.sfprintf "%s_%s_%a%d"
-                    prefix name Chunk.pretty chunk i in
+                let l_name = Pretty_utils.sfprintf "%s_%s_%s%d"
+                    prefix name (Chunk.basename_of_chunk chunk) i in
                 let l_lemma = F.p_hyps conditions (p_equal value1 value2) in
                 Definitions.define_lemma {
                   l_kind = Admit ;
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 50a414265a5c5538e3659b30fba7ca427a996905..aaead6141ed039b547d2c8e4e3348e9452492dea 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -147,7 +147,7 @@ struct
     | T_alloc -> 12
     | T_init -> 13
   let hash = rank
-  let name = function
+  let basename = function
     | M_int i when Ctypes.is_char i -> "Mchar"
     | M_int _ -> "Mint"
     | M_f32 -> "Mf32"
@@ -157,10 +157,9 @@ struct
     | T_init -> "Init"
   let compare a b = rank a - rank b
   let equal = (=)
-  let pretty fmt c = Format.pp_print_string fmt (name c)
-  let detailed_pretty fmt = function
+  let pretty fmt = function
     | M_int i -> Format.fprintf fmt "M%a" Ctypes.pp_int i
-    | m -> Format.pp_print_string fmt (name m)
+    | m -> Format.pp_print_string fmt (basename m)
   let val_of_chunk = function
     | M_int _ -> L.Int
     | M_f32 -> Cfloat.tau_of_float Ctypes.Float32
@@ -175,7 +174,7 @@ struct
     | M_f64 -> L.Array(t_addr,Cfloat.tau_of_float Ctypes.Float64)
     | T_alloc -> t_malloc
     | T_init -> t_init
-  let basename_of_chunk = name
+  let basename_of_chunk = basename
   let is_framed _ = false
 end
 
@@ -1213,7 +1212,7 @@ and lookup_lv e = try lookup_a e with Not_found -> Sigs.(Mmem e,[])
 let mchunk c =
   match c with
   | T_init -> Sigs.Mchunk (Pretty_utils.to_string Chunk.pretty c, KInit)
-  | _ -> Sigs.Mchunk (Pretty_utils.to_string Chunk.detailed_pretty c, KValue)
+  | _ -> Sigs.Mchunk (Pretty_utils.to_string Chunk.pretty c, KValue)
 
 let lookup s e =
   try mchunk (Tmap.find e s)