# 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;