src/Pure/Isar/generic_target.ML

     val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
 
     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;
 
 fun check_mixfix ctxt (b, extra_tfrees) mx =
   if null extra_tfrees then mx
   else
    (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);
 
 fun check_mixfix_global (b, no_params) mx =

     val xs = Variable.add_fixed lthy rhs' [];
     val T = Term.fastype_of rhs;
     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;
     val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) xs);
     val params = type_params @ term_params;

     val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms;
 
     (*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;
     val (th'' :: vs) =
       (th' :: map (Drule.mk_term o Thm.cterm_of ctxt) (map Logic.mk_type tfrees @ frees))