diff --git a/src/parse/Parse.sig b/src/parse/Parse.sig
index dcd3908a08..aad5235c65 100644
--- a/src/parse/Parse.sig
+++ b/src/parse/Parse.sig
@@ -196,6 +196,7 @@ signature Parse = sig
   val pp_thm : thm pprinter
   val stdprinters : ((term -> string) * (hol_type -> string)) option
 
+  val pp_type_without_colon   : hol_type pprinter
   val term_pp_with_delimiters : term pprinter -> term pprinter
   val type_pp_with_delimiters : hol_type pprinter -> hol_type pprinter
   val get_term_printer : unit -> term pprinter
diff --git a/src/parse/Parse.sml b/src/parse/Parse.sml
index e69e8cad75..4b7357d03b 100644
--- a/src/parse/Parse.sml
+++ b/src/parse/Parse.sml
@@ -170,6 +170,15 @@ fun update_type_fns () =
 
 val dflt_pinfo = term_pp_utils.dflt_pinfo
 
+fun pp_type_without_colon ty =
+  let
+    open smpp
+    val _ = update_type_fns()
+    val mptr = !type_printer (!current_backend) ty
+  in
+    lower mptr dflt_pinfo |> valOf |> #1
+  end
+
 fun pp_type ty =
   let
     open smpp