diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 9009c9ac71197952e6659c2505935138976c13d0..898e8129f48a818fca7e62309754abea13d9d099 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -38,7 +38,7 @@ type localizable =
   | PIP of Property.t
 
 module Localizable =
-  Datatype.Make
+  Datatype.Make_with_collections
     (struct
       include Datatype.Undefined
       type t = localizable
diff --git a/src/kernel_services/ast_printing/printer_tag.mli b/src/kernel_services/ast_printing/printer_tag.mli
index befac9be01d0e1273a2a189ec5dc4a43bf467b50..074ec5c58ef05e47a804294db77e5b7fd1903f03 100644
--- a/src/kernel_services/ast_printing/printer_tag.mli
+++ b/src/kernel_services/ast_printing/printer_tag.mli
@@ -41,7 +41,7 @@ type localizable =
                           definitions. *)
   | PIP of Property.t
 
-module Localizable: Datatype.S with type t = localizable
+module Localizable: Datatype.S_with_collections with type t = localizable
 
 val kf_of_localizable : localizable -> kernel_function option
 val ki_of_localizable : localizable -> kinstr
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index acd120718217d88e3a67b7a741b4fbf57166fbb7..21870f3dfc505003653c9a64285bd3f3733552ca 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -45,13 +45,18 @@ module Marker =
 struct
 
   open Printer_tag
-  module Hmap = Hashtbl.Make(Localizable)
 
-  type index = string Hmap.t * (string,localizable) Hashtbl.t
+  type index = {
+    tags : string Localizable.Hashtbl.t ;
+    locs : (string,localizable) Hashtbl.t ;
+  }
 
   let kid = ref 0
 
-  let index () = Hmap.create 0, Hashtbl.create 0
+  let index () = {
+    tags = Localizable.Hashtbl.create 0 ;
+    locs = Hashtbl.create 0 ;
+  }
 
   module TYPE : Datatype.S with type t = index =
     Datatype.Make
@@ -81,15 +86,15 @@ struct
     | PIP _ -> Printf.sprintf "#p%d" (incr kid ; !kid)
 
   let create loc =
-    let (tags,index) = STATE.get () in
-    try Hmap.find tags loc
+    let { tags ; locs } = STATE.get () in
+    try Localizable.Hashtbl.find tags loc
     with Not_found ->
       let tag = create_tag loc in
-      Hmap.add tags loc tag ;
-      Hashtbl.add index tag loc ;
+      Localizable.Hashtbl.add tags loc tag ;
+      Hashtbl.add locs tag loc ;
       tag
 
-  let lookup = Hashtbl.find (STATE.get() |> snd)
+  let lookup = Hashtbl.find (STATE.get()).locs
 
   type t = localizable
   let syntax = Sy.publish ~page:Data.page ~name:"marker"