diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index ca5511407cf9749bcf094ac03e601433c1a1d16c..1789b851855f8454a486b6ffd51ddb6778df15c2 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -4191,9 +4191,14 @@ struct
     | LDlemma (x,labels, poly, {tp_kind = kind; tp_statement = e}) ->
       if Logic_env.Lemmas.mem x then begin
         let old_def = Logic_env.Lemmas.find x in
+        let old_kind = match old_def with
+          | Dlemma(_,_,_,{tp_kind },_,_) -> tp_kind
+          | _ -> Assert in
         let old_loc = Cil_datatype.Global_annotation.loc old_def in
-        C.error loc "lemma %s is already registered (%a)"
-          x Cil_datatype.Location.pretty old_loc
+        C.error loc "%a %s is already registered as %a (%a)"
+          Cil_printer.pp_lemma_kind kind x
+          Cil_printer.pp_lemma_kind old_kind
+          Cil_datatype.Location.pretty old_loc
       end;
       let labels,env = annot_env loc labels poly in
       let p = Logic_const.toplevel_predicate ~kind (predicate env e) in
diff --git a/tests/spec/oracle/axiom_redef_bts1005.res.oracle b/tests/spec/oracle/axiom_redef_bts1005.res.oracle
index d6bf2400ede3dba79a3f443e7ae434551d0639de..01b443473c69f0239760d31fade993604a9b6f9b 100644
--- a/tests/spec/oracle/axiom_redef_bts1005.res.oracle
+++ b/tests/spec/oracle/axiom_redef_bts1005.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing tests/spec/axiom_redef_bts1005.i (no preprocessing)
 [kernel:annot-error] tests/spec/axiom_redef_bts1005.i:5: Warning: 
-  lemma inj1 is already registered (tests/spec/axiom_redef_bts1005.i:4). Ignoring global annotation
+  axiom inj1 is already registered as axiom (tests/spec/axiom_redef_bts1005.i:4). Ignoring global annotation
 /* Generated by Frama-C */