diff --git a/printer.ml b/printer.ml
index 2ab9a607..f10aab8c 100644
--- a/printer.ml
+++ b/printer.ml
@@ -144,6 +144,12 @@ let typify_universal_set = ref true;;
 
 let print_all_thm = ref true;;
 
+(* ------------------------------------------------------------------------- *)
+(* Flag controlling whether invented type variables must explicitly appear.  *)
+(* ------------------------------------------------------------------------- *)
+
+let print_invented_type_vars = ref false;;
+
 (* ------------------------------------------------------------------------- *)
 (* Get the name of a constant or variable.                                   *)
 (* ------------------------------------------------------------------------- *)
@@ -422,7 +428,17 @@ let pp_print_term =
       else if (is_const hop || is_var hop) && args = [] then
         let s' = if parses_as_binder s || can get_infix_status s || is_prefix s
                  then "("^s^")" else s in
-        pp_print_string fmt s'
+        let rec has_invented_typevar (ty:hol_type): bool =
+          if is_vartype ty then (dest_vartype ty).[0] = '?'
+          else List.exists has_invented_typevar (snd (dest_type ty)) in
+        if !print_invented_type_vars && has_invented_typevar (type_of hop) then
+          (pp_print_string fmt "(";
+          pp_print_string fmt s';
+          pp_print_string fmt ":";
+          pp_print_type fmt (type_of hop);
+          pp_print_string fmt ")")
+        else
+          pp_print_string fmt s'
       else
         let l,r = dest_comb tm in
         (pp_open_hvbox fmt 0;