diff --git a/src/datatype/Datatype.sig b/src/datatype/Datatype.sig
index 5d68526ea7..90eb3fea44 100644
--- a/src/datatype/Datatype.sig
+++ b/src/datatype/Datatype.sig
@@ -34,7 +34,8 @@ sig
  (* into their tyinfo to do inequality resolution.                            *)
  (*---------------------------------------------------------------------------*)
 
- val typecheck_listener : (string Symtab.table -> ParseDatatype.pretype -> hol_type -> unit) ref
+ val typecheck_listener :
+     (string Symtab.table * ParseDatatype.pretype * hol_type) Listener.t
  val build_tyinfos : typeBase
                          -> {induction:thm, recursion:thm}
                            -> tyinfo list
diff --git a/src/datatype/Datatype.sml b/src/datatype/Datatype.sml
index a4de694e22..328c43273d 100644
--- a/src/datatype/Datatype.sml
+++ b/src/datatype/Datatype.sml
@@ -179,7 +179,8 @@ fun ast_tyvar_strings (dAQ ty) = map dest_vartype $ type_vars ty
   | ast_tyvar_strings (dTyop {Args, ...}) =
       List.concat (map ast_tyvar_strings Args)
 
-val typecheck_listener = ref (fn _: string Symtab.table => fn _: pretype => fn _:hol_type => ())
+val typecheck_listener : (string Symtab.table * pretype * hol_type) Listener.t =
+    Listener.new_listener()
 
 local
   fun strvariant avoids s = if mem s avoids then strvariant avoids (s ^ "a")
@@ -223,7 +224,7 @@ fun to_tyspecs ASTs =
                                        Args = map (mk_hol_ty d) Args}
      fun mk_hol_type d pty = let
        val ty = mk_hol_ty d pty
-       val _ = !typecheck_listener d pty ty
+       val _ = Listener.call_listener typecheck_listener (d, pty, ty)
      in
        if Theory.uptodate_type ty then ty
        else let val tyname = #1 (dest_type ty)
diff --git a/src/parse/ParseDatatype.sig b/src/parse/ParseDatatype.sig
index 5c01a220f4..ea522dadbd 100644
--- a/src/parse/ParseDatatype.sig
+++ b/src/parse/ParseDatatype.sig
@@ -41,6 +41,6 @@ val hparse : type_grammar.grammar -> Type.hol_type Portable.quotation ->
   or a type-constant of arity 0, or one of the types being defined.
 *)
 
-val parse_listener : (AST list -> unit) ref
+val parse_listener : (AST list) Listener.t
 
 end
diff --git a/src/parse/ParseDatatype.sml b/src/parse/ParseDatatype.sml
index 434fa8628b..01cfd4963e 100644
--- a/src/parse/ParseDatatype.sml
+++ b/src/parse/ParseDatatype.sml
@@ -350,13 +350,13 @@ end
 fun hide_tynames q G0 =
   List.foldl (uncurry type_grammar.hide_tyop) G0 (extract_tynames q)
 
-val parse_listener = ref (fn _: (string * datatypeForm) list => ())
+val parse_listener : AST list Listener.t = Listener.new_listener ()
 
 fun core_parse G0 phrase_p q = let
   val G = hide_tynames q G0
   val qb = qbuf.new_buffer q
   val result = termsepby1 ";" base_tokens.BT_EOI (parse_g G phrase_p) qb
-  val _ = !parse_listener result
+  val _ = Listener.call_listener parse_listener result
 in
   case qbuf.current qb of
       (base_tokens.BT_EOI,_) => result
diff --git a/src/parse/Preterm.sig b/src/parse/Preterm.sig
index 677d78cd35..d1e779f52b 100644
--- a/src/parse/Preterm.sig
+++ b/src/parse/Preterm.sig
@@ -70,7 +70,7 @@ sig
     ((term -> string) * (hol_type -> string)) option -> preterm -> term errM
   val typecheckS : preterm -> term seqM
 
-  val typecheck_listener : (preterm -> Pretype.Env.t -> unit) ref
+  val typecheck_listener : (preterm * Pretype.Env.t) Listener.t
   val last_tcerror : (tcheck_error * locn.locn) option ref
 
 end
diff --git a/src/parse/Preterm.sml b/src/parse/Preterm.sml
index 1f0aef4c6a..8a2e876051 100644
--- a/src/parse/Preterm.sml
+++ b/src/parse/Preterm.sml
@@ -858,7 +858,8 @@ fun remove_case_magic tm =
     else tm
 
 val post_process_term = ref (I : term -> term);
-val typecheck_listener = ref (fn _:preterm => fn _:Pretype.Env.t => ());
+val typecheck_listener : (preterm * Pretype.Env.t) Listener.t =
+    Listener.new_listener()
 
 fun typecheck pfns ptm0 =
   let
@@ -869,7 +870,7 @@ fun typecheck pfns ptm0 =
           overloading_resolution ptm0 >-                     (fn (ptm,b) =>
           (report_ovl_ambiguity b >> to_term ptm) >-         (fn t =>
          fn e => (
-          !typecheck_listener ptm e;
+          ignore (Listener.call_listener typecheck_listener (ptm, e));
           errormonad.Some(e, !post_process_term t)))))
   end
 
@@ -881,7 +882,7 @@ fun typecheckS ptm =
     lift (!post_process_term o remove_case_magic)
          (fromErr TC' >> overloading_resolutionS ptm >-
           (fn ptm' => fromErr (errormonad.bind (to_term ptm', fn t => fn e => (
-            !typecheck_listener ptm' e;
+            ignore (Listener.call_listener typecheck_listener (ptm', e));
             errormonad.Some(e, t))))))
   end
 
diff --git a/src/tfl/src/Defn.sml b/src/tfl/src/Defn.sml
index 06aede8ef2..34e03f986d 100644
--- a/src/tfl/src/Defn.sml
+++ b/src/tfl/src/Defn.sml
@@ -1779,7 +1779,7 @@ fun defn_absyn_to_term a = let
       overloading_resolution ptm >- (fn (pt,b) =>
       report_ovl_ambiguity b     >>
       to_term pt                 >- (fn t => fn e => (
-      !Preterm.typecheck_listener pt e;
+      ignore (Listener.call_listener Preterm.typecheck_listener (pt, e));
       return (t |> remove_case_magic |> !post_process_term) e)))
     end
   val M =