# HG changeset patch
# User wenzelm
# Date 1631219355 -7200
# Node ID 42db84eaee2ddd3429a97bb2f5ce69827a796941
# Parent  a123db647573d9ef7f43ea2dcf4a5bfbc8441e90
clarified order of extra type variables, following names more often than occurrences;

diff -r a123db647573 -r 42db84eaee2d src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Sep 09 22:12:05 2021 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Sep 09 22:29:15 2021 +0200
@@ -699,7 +699,7 @@
     val type_tfrees = TFrees.build (fold TFrees.add_tfreesT Ts);
     val extra_tfrees =
       TFrees.build (TFrees.add_tfrees_unless (TFrees.defined type_tfrees) body)
-      |> TFrees.list_set |> sort_by #1 |> map TFree;
+      |> TFrees.keys |> map TFree;
     val predT = map Term.itselfT extra_tfrees ---> Ts ---> bodyT;
 
     val args = map Logic.mk_type extra_tfrees @ map Free xs;
@@ -817,12 +817,12 @@
     val type_tfrees = TFrees.build (fold (TFrees.add_tfreesT o #2) parms);
     val extra_tfrees =
       TFrees.build (fold (TFrees.add_tfrees_unless (TFrees.defined type_tfrees)) exts')
-    val extraTs = TFrees.list_set_rev extra_tfrees;
+      |> TFrees.keys;
     val _ =
-      if null extraTs then ()
+      if null extra_tfrees then ()
       else warning ("Additional type variable(s) in locale specification " ^
           Binding.print binding ^ ": " ^
-          commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_by #1 extraTs)));
+          commas (map (Syntax.string_of_typ ctxt' o TFree) extra_tfrees));
 
     val predicate_binding =
       if Binding.is_empty raw_predicate_binding then binding
@@ -862,7 +862,7 @@
     val axioms = map (Element.conclude_witness pred_ctxt) b_axioms;
 
     val loc_ctxt = thy'
-      |> Locale.register_locale binding (extraTs, params)
+      |> Locale.register_locale binding (extra_tfrees, params)
           (asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps')
       |> Named_Target.init includes name
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
diff -r a123db647573 -r 42db84eaee2d src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Thu Sep 09 22:12:05 2021 +0200
+++ b/src/Pure/primitive_defs.ML	Thu Sep 09 22:29:15 2021 +0200
@@ -54,7 +54,7 @@
     val rhs_extrasT =
       TFrees.build (rhs |> TFrees.add_tfrees_unless
         (fn (a, S) => check_tfree a orelse TFrees.defined head_tfrees (a, S)))
-      |> TFrees.list_set_rev |> map TFree;
+      |> TFrees.keys |> map TFree;
   in
     if not (check_head head) then
       err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head])
diff -r a123db647573 -r 42db84eaee2d src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Sep 09 22:12:05 2021 +0200
+++ b/src/Pure/theory.ML	Thu Sep 09 22:29:15 2021 +0200
@@ -247,7 +247,7 @@
     val lhs_vars = TFrees.build (fold TFrees.add_tfreesT (snd lhs));
     val rhs_extras =
       TFrees.build (rhs |> fold (fold (TFrees.add_tfreesT_unless (TFrees.defined lhs_vars)) o snd))
-      |> TFrees.list_set_rev;
+      |> TFrees.keys;
     val _ =
       if null rhs_extras then ()
       else error ("Specification depends on extra type variables: " ^