tuned;

--- a/src/Pure/variable.ML	Thu Aug 26 14:45:19 2021 +0200
+++ b/src/Pure/variable.ML	Thu Aug 26 14:52:15 2021 +0200
@@ -516,14 +516,14 @@
     val still_fixed = not o is_newly_fixed inner outer;
 
     val gen_fixes =
-      Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? cons y)
-        (fixes_of inner) [];
+      Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? Symtab.insert_set y)
+        (fixes_of inner) Symtab.empty;
 
     val type_occs_inner = type_occs_of inner;
     fun gen_fixesT ts =
       Symtab.fold (fn (a, xs) =>
         if declared_outer a orelse exists still_fixed xs
-        then I else cons a) (fold decl_type_occs ts type_occs_inner) [];
+        then I else Symtab.insert_set a) (fold decl_type_occs ts type_occs_inner) Symtab.empty;
   in (gen_fixesT, gen_fixes) end;
 
 fun exportT_inst inner outer = #1 (export_inst inner outer);
@@ -534,7 +534,7 @@
     val maxidx = maxidx_of outer;
   in
     fn ts => ts |> map
-      (Term_Subst.generalize (Symtab.make_set (mk_tfrees ts), Symtab.empty)
+      (Term_Subst.generalize (mk_tfrees ts, Symtab.empty)
         (fold (Term.fold_types Term.maxidx_typ) ts maxidx + 1))
   end;
 
@@ -544,17 +544,17 @@
     val maxidx = maxidx_of outer;
   in
     fn ts => ts |> map
-      (Term_Subst.generalize (Symtab.make_set (mk_tfrees ts), Symtab.make_set tfrees)
+      (Term_Subst.generalize (mk_tfrees ts, tfrees)
         (fold Term.maxidx_term ts maxidx + 1))
   end;
 
 fun export_prf inner outer prf =
   let
     val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer;
-    val tfrees = Symtab.make_set (mk_tfrees []);
+    val tfrees = mk_tfrees [];
     val maxidx = maxidx_of outer;
     val idx = Proofterm.maxidx_proof prf maxidx + 1;
-    val gen_term = Term_Subst.generalize_same (tfrees, Symtab.make_set frees) idx;
+    val gen_term = Term_Subst.generalize_same (tfrees, frees) idx;
     val gen_typ = Term_Subst.generalizeT_same tfrees idx;
   in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end;
 
@@ -563,9 +563,9 @@
   let
     val tfrees = mk_tfrees (map Thm.full_prop_of ths);
     val idx = fold Thm.maxidx_thm ths maxidx + 1;
-  in map (Thm.generalize (Symtab.make_set tfrees, Symtab.make_set frees) idx) ths end;
+  in map (Thm.generalize (tfrees, frees) idx) ths end;
 
-fun exportT inner outer = gen_export (exportT_inst inner outer, []) (maxidx_of outer);
+fun exportT inner outer = gen_export (exportT_inst inner outer, Symtab.empty) (maxidx_of outer);
 fun export inner outer = gen_export (export_inst inner outer) (maxidx_of outer);
 
 fun export_morphism inner outer =