# HG changeset patch
# User wenzelm
# Date 1631282229 -7200
# Node ID 8d1e27a23dd1031aa33003f6217c06a8dfe05c1c
# Parent  019fe82386568c5e085bdba6f26e7a1c76892ba8
clarified order of extra TFrees: underlying fast_string_ord coincides with Name.invent (e.g. from type inference);

diff -r 019fe8238656 -r 8d1e27a23dd1 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Fri Sep 10 15:08:09 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML	Fri Sep 10 15:57:09 2021 +0200
@@ -98,7 +98,7 @@
     val type_tfrees = TFrees.build (TFrees.add_tfreesT (Term.fastype_of u));
     val extra_tfrees =
       TFrees.build (TFrees.add_tfrees_unless (TFrees.defined type_tfrees) u)
-      |> TFrees.list_set;
+      |> TFrees.keys;
     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
   in (global_rhs, (extra_tfrees, (type_params, term_params))) end;
 
@@ -108,7 +108,7 @@
    (if Context_Position.is_visible ctxt then
       warning
         ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
-          commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^
+          commas (map (Syntax.string_of_typ ctxt o TFree) extra_tfrees) ^
           (if Mixfix.is_empty mx then ""
            else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)))
     else (); NoSyn);
@@ -264,7 +264,7 @@
     val type_tfrees = TFrees.build (TFrees.add_tfreesT T #> fold (TFrees.add_tfreesT o #2) xs);
     val extra_tfrees =
       TFrees.build (rhs |> TFrees.add_tfrees_unless (TFrees.defined type_tfrees))
-      |> TFrees.list_set;
+      |> TFrees.keys;
     val mx' = check_mixfix lthy (b, extra_tfrees) mx;
 
     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
@@ -308,7 +308,7 @@
     (*export fixes*)
     val tfrees =
       TFrees.build (Thm.fold_terms {hyps = true} TFrees.add_tfrees th')
-      |> TFrees.list_set_rev |> map TFree;
+      |> TFrees.keys |> map TFree;
     val frees =
       Frees.build (Thm.fold_terms {hyps = true} Frees.add_frees th')
       |> Frees.list_set_rev |> map Free;