diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index b0954e3174e41a9ccb7bbe1afeb2d5c33a483de3..8a0936ec6f42bb669fedfb1d0ac3efa0a2a694f6 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -843,11 +843,9 @@ let () = Information.register
     ~title:"Type Definition"
     begin fun fmt loc ->
       match loc with
-      | PGlobal
-          (( GType _
-           | GCompTag _ | GCompTagDecl _
-           | GEnumTag _ | GEnumTagDecl _
-           ) as g) -> Printer.pp_global fmt g
+      | PType (TNamed _ as ty)
+      | PGlobal (GType({ ttype = ty },_)) ->
+        Printer.pp_typ fmt (Cil.unrollType ty)
       | _ -> raise Not_found
     end