Add a flag for printing invented type vars in a term

This patch adds a new bool ref flag `print_invented_type_vars`.
If it is set to true, it makes a term printer print the type of any subexpression if the type contains an invented type variable.

```
\# `word_join (word 10:int64) (word 20:int64)`;;
Warning: inventing type variables
val it : term = `word_join (word 10) (word 20)`
\# print_invented_type_vars := true;;
val it : unit = ()
\# `word_join (word 10:int64) (word 20:int64)`;;
Warning: inventing type variables
val it : term =
  `(word_join:(64)word->(64)word->(?194593)word) (word 10) (word 20)`
\# `word_join (word 10:int64) (word 20:int64):int128`;;
val it : term = `word_join (word 10) (word 20)`
```

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;