more conservative type names, e.g. relevant for Isabelle/MMT export;

--- a/src/Pure/more_thm.ML	Tue Oct 22 11:14:52 2019 +0200
+++ b/src/Pure/more_thm.ML	Tue Oct 22 20:08:25 2019 +0200
@@ -516,7 +516,7 @@
 fun stripped_sorts thy t =
   let
     val tfrees = rev (Term.add_tfrees t []);
-    val tfrees' = map (fn a => (a, [])) (Name.invent Name.context Name.aT (length tfrees));
+    val tfrees' = map (fn a => (a, [])) (Name.variant_list [] (map #1 tfrees));
     val recover =
       map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S))))
         tfrees' tfrees;