# HG changeset patch
# User wenzelm
# Date 1571767705 -7200
# Node ID 539dfd4c166b0b6f7e0ceb44982c6cb402d72379
# Parent  05810acd48585d058bc2309735574f47a9ba552e
more conservative type names, e.g. relevant for Isabelle/MMT export;

diff -r 05810acd4858 -r 539dfd4c166b src/Pure/more_thm.ML
--- 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;