# HG changeset patch
# User wenzelm
# Date 1630688253 -7200
# Node ID c49134ee16c1f9bd82f3f888732d6ad0f4696dbb
# Parent  1d25be2353e16e89c01ff85e5a50b37fe80a610c
more scalable data structure (but: rarely used many arguments);

diff -r 1d25be2353e1 -r c49134ee16c1 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -45,7 +45,7 @@
      ('a -> thm -> 'b Seq.seq) -> 'a -> thm -> 'b Seq.seq
   val try_dest_Trueprop : term -> term
 
-  val type_devar : ((indexname * sort) * typ) list -> term -> term
+  val type_devar : typ Term_Subst.TVars.table -> term -> term
   val diff_and_instantiate : Proof.context -> thm -> term -> term -> thm
 
   val batter_tac : Proof.context -> int -> tactic
@@ -545,7 +545,7 @@
        end)
 
 (*Instantiate type variables in a term, based on a type environment*)
-fun type_devar (tyenv : ((indexname * sort) * typ) list) (t : term) : term =
+fun type_devar tyenv (t : term) : term =
   case t of
       Const (s, ty) => Const (s, Term_Subst.instantiateT tyenv ty)
     | Free (s, ty) => Free (s, Term_Subst.instantiateT tyenv ty)
@@ -573,7 +573,7 @@
     val typeval = map (fn (v, T) => (dest_TVar v, Thm.ctyp_of ctxt T)) type_pairing
 
     val typeval_env =
-      map (apfst dest_TVar) type_pairing
+      Term_Subst.TVars.table (map (apfst dest_TVar) type_pairing)
     (*valuation of term variables*)
     val termval =
       map (apfst (dest_Var o type_devar typeval_env)) term_pairing
diff -r 1d25be2353e1 -r c49134ee16c1 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -78,8 +78,8 @@
     val (instT, lthy2) = lthy1
       |> Variable.declare_names fixed_crel
       |> Variable.importT_inst (param_rel_subst :: args_subst)
-    val args_fixed = (map (Term_Subst.instantiate (instT, []))) args_subst
-    val param_rel_fixed = Term_Subst.instantiate (instT, []) param_rel_subst
+    val args_fixed = (map (Term_Subst.instantiate (instT, Term_Subst.Vars.empty))) args_subst
+    val param_rel_fixed = Term_Subst.instantiate (instT, Term_Subst.Vars.empty) param_rel_subst
     val rty = (domain_type o fastype_of) param_rel_fixed
     val relcomp_op = Const (\<^const_name>\<open>relcompp\<close>, 
           (rty --> rty' --> HOLogic.boolT) --> 
@@ -295,7 +295,7 @@
     let
       val tvars = rev (subtract op= exclude (fold Term.add_tvars ts []))
       val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt
-    in (tvars ~~ map TFree tfrees, ctxt') end
+    in (Term_Subst.TVars.table (tvars ~~ map TFree tfrees), ctxt') end
   
   fun import_inst_exclude exclude ts ctxt =
     let
@@ -304,7 +304,7 @@
       val vars = map (apsnd (Term_Subst.instantiateT instT)) 
         (rev (subtract op= exclude (fold Term.add_vars ts [])))
       val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt'
-      val inst = vars ~~ map Free (xs ~~ map #2 vars)
+      val inst = Term_Subst.Vars.table (vars ~~ map Free (xs ~~ map #2 vars))
     in ((instT, inst), ctxt'') end
   
   fun import_terms_exclude exclude ts ctxt =
diff -r 1d25be2353e1 -r c49134ee16c1 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -1072,7 +1072,10 @@
                   " (trying to match " ^ Syntax.string_of_typ ctxt' (fastype_of pred') ^
                   " and " ^ Syntax.string_of_typ ctxt' (fastype_of pred) ^ ")" ^
                   " in " ^ Thm.string_of_thm ctxt' th)
-          in map (fn (xi, (S, T)) => ((xi, S), T)) (Vartab.dest subst) end
+          in
+            Vartab.fold (fn (xi, (S, T)) => Term_Subst.TVars.add ((xi, S), T))
+              subst Term_Subst.TVars.empty
+          end
         fun instantiate_typ th =
           let
             val (pred', _) = strip_intro_concl th
@@ -1080,7 +1083,10 @@
               if not (fst (dest_Const pred) = fst (dest_Const pred')) then
                 raise Fail "Trying to instantiate another predicate"
               else ()
-          in Thm.instantiate (map (apsnd (Thm.ctyp_of ctxt')) (subst_of (pred', pred)), []) th end
+            val instT =
+              Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T))
+                (subst_of (pred', pred)) [];
+          in Thm.instantiate (instT, []) th end
         fun instantiate_ho_args th =
           let
             val (_, args') =
@@ -1088,7 +1094,7 @@
             val ho_args' = map dest_Var (ho_args_of_typ T args')
           in Thm.instantiate ([], ho_args' ~~ map (Thm.cterm_of ctxt') ho_args) th end
         val outp_pred =
-          Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
+          Term_Subst.instantiate (subst_of (inp_pred, pred), Term_Subst.Vars.empty) inp_pred
         val ((_, ths'), ctxt1) =
           Variable.import false (map (instantiate_typ #> instantiate_ho_args) ths) ctxt'
       in
diff -r 1d25be2353e1 -r c49134ee16c1 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/Isar/expression.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -190,7 +190,8 @@
       (type_parms ~~ map Logic.dest_type type_parms'')
       |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T));
     val cert_inst =
-      ((map #1 params ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'')
+      ((map #1 params ~~
+        map (Term_Subst.instantiateT_frees (Term_Subst.TFrees.table instT)) parm_types) ~~ insts'')
       |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t));
   in
     (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $>
diff -r 1d25be2353e1 -r c49134ee16c1 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/Isar/generic_target.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -317,14 +317,17 @@
       chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs)
       |>> map Logic.dest_type;
 
-    val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
-    val inst =
+    val instT =
+      fold2 (fn a => fn b => (case a of TVar v => Term_Subst.TVars.add (v, b) | _ => I))
+        tvars tfrees Term_Subst.TVars.empty;
+    val cinstT = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt T)) instT [];
+    val cinst =
       map_filter
         (fn (Var (xi, T), t) =>
           SOME ((xi, Term_Subst.instantiateT instT T),
             Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t))
         | _ => NONE) (vars ~~ frees);
-    val result' = Thm.instantiate (map (apsnd (Thm.ctyp_of ctxt)) instT, inst) result;
+    val result' = Thm.instantiate (cinstT, cinst) result;
 
     (*import assumes/defines*)
     val result'' =
diff -r 1d25be2353e1 -r c49134ee16c1 src/Pure/Isar/subgoal.ML
--- a/src/Pure/Isar/subgoal.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/Isar/subgoal.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -55,8 +55,8 @@
       else ([], goal);
     val text = asms @ (if do_concl then [concl] else []);
 
-    val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
-    val schematic_terms = map (apsnd (Thm.cterm_of ctxt3)) (#2 inst);
+    val ((_, inst), ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
+    val schematic_terms = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst [];
 
     val schematics = (schematic_types, schematic_terms);
     val asms' = map (Thm.instantiate_cterm schematics) asms;
diff -r 1d25be2353e1 -r c49134ee16c1 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -119,7 +119,8 @@
       |> Proof_Context.add_fixes_cmd raw_fixes;
 
     (*explicit type instantiations*)
-    val instT1 = Term_Subst.instantiateT (map (read_type ctxt1 tvars) type_insts);
+    val instT1 =
+      Term_Subst.instantiateT (Term_Subst.TVars.table (map (read_type ctxt1 tvars) type_insts));
     val vars1 = map (apsnd instT1) vars;
 
     (*term instantiations*)
@@ -128,10 +129,12 @@
     val ((ts, inferred), ctxt2) = read_terms ss Ts ctxt1;
 
     (*implicit type instantiations*)
-    val instT2 = Term_Subst.instantiateT inferred;
+    val instT2 = Term_Subst.instantiateT (Term_Subst.TVars.table inferred);
     val vars2 = map (apsnd instT2) vars1;
     val inst2 =
-      Term_Subst.instantiate ([], map2 (fn (xi, _) => fn t => ((xi, Term.fastype_of t), t)) xs ts)
+      Term_Subst.instantiate (Term_Subst.TVars.empty,
+        fold2 (fn (xi, _) => fn t => Term_Subst.Vars.add ((xi, Term.fastype_of t), t))
+          xs ts Term_Subst.Vars.empty)
       #> Envir.beta_norm;
 
     val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
diff -r 1d25be2353e1 -r c49134ee16c1 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/consts.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -225,9 +225,11 @@
 fun instance consts (c, Ts) =
   let
     val declT = type_scheme consts c;
-    val vars = map Term.dest_TVar (typargs consts (c, declT));
-    val inst = vars ~~ Ts handle ListPair.UnequalLengths =>
-      raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
+    val args = typargs consts (c, declT);
+    val inst =
+      fold2 (fn a => fn T => Term_Subst.TVars.add (Term.dest_TVar a, T))
+        args Ts Term_Subst.TVars.empty
+      handle ListPair.UnequalLengths => raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
   in declT |> Term_Subst.instantiateT inst end;
 
 fun dummy_types consts =
diff -r 1d25be2353e1 -r c49134ee16c1 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/drule.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -214,11 +214,15 @@
 
         val tvars = fold Thm.add_tvars ths [];
         fun the_tvar v = the (find_first (fn cT => v = dest_TVar (Thm.typ_of cT)) tvars);
-        val instT' = map (fn (v, TVar (b, _)) => (v, Thm.rename_tvar b (the_tvar v))) instT;
+        val instT' =
+          (instT, []) |-> Term_Subst.TVars.fold (fn (v, TVar (b, _)) =>
+            cons (v, Thm.rename_tvar b (the_tvar v)));
 
         val vars = fold (Thm.add_vars o Thm.instantiate (instT', [])) ths [];
         fun the_var v = the (find_first (fn ct => v = dest_Var (Thm.term_of ct)) vars);
-        val inst' = map (fn (v, Var (b, _)) => (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v)))) inst;
+        val inst' =
+          (inst, []) |-> Term_Subst.Vars.fold (fn (v, Var (b, _)) =>
+            cons (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v))));
       in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (instT', inst')) ths end;
 
 val zero_var_indexes = singleton zero_var_indexes_list;
diff -r 1d25be2353e1 -r c49134ee16c1 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/more_thm.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -467,8 +467,9 @@
       handle TERM (msg, _) => raise THM (msg, 0, [th]);
 
     val instT = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
+    val instantiateT = Term_Subst.instantiateT (Term_Subst.TVars.table instT);
     val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
-      let val T' = Term_Subst.instantiateT instT T
+      let val T' = instantiateT T
       in (((a, i), T'), Thm.global_cterm_of thy (Free ((a, T')))) end);
   in Thm.instantiate (map (apsnd (Thm.global_ctyp_of thy)) instT, inst) th end;
 
diff -r 1d25be2353e1 -r c49134ee16c1 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/morphism.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -137,12 +137,18 @@
 fun instantiate_frees_morphism ([], []) = identity
   | instantiate_frees_morphism (cinstT, cinst) =
       let
-        val instT = map (apsnd Thm.typ_of) cinstT;
-        val inst = map (apsnd Thm.term_of) cinst;
+        val instT =
+          fold (fn (v, cT) => Term_Subst.TFrees.add (v, Thm.typ_of cT))
+            cinstT Term_Subst.TFrees.empty;
+        val inst =
+          fold (fn (v, ct) => Term_Subst.Frees.add (v, Thm.term_of ct))
+            cinst Term_Subst.Frees.empty;
       in
         morphism "instantiate_frees"
           {binding = [],
-           typ = if null instT then [] else [Term_Subst.instantiateT_frees instT],
+           typ =
+            if Term_Subst.TFrees.is_empty instT then []
+            else [Term_Subst.instantiateT_frees instT],
            term = [Term_Subst.instantiate_frees (instT, inst)],
            fact = [map (Thm.instantiate_frees (cinstT, cinst))]}
       end;
@@ -150,12 +156,18 @@
 fun instantiate_morphism ([], []) = identity
   | instantiate_morphism (cinstT, cinst) =
       let
-        val instT = map (apsnd Thm.typ_of) cinstT;
-        val inst = map (apsnd Thm.term_of) cinst;
+        val instT =
+          fold (fn (v, cT) => Term_Subst.TVars.add (v, Thm.typ_of cT))
+            cinstT Term_Subst.TVars.empty;
+        val inst =
+          fold (fn (v, ct) => Term_Subst.Vars.add (v, Thm.term_of ct))
+            cinst Term_Subst.Vars.empty;
       in
         morphism "instantiate"
           {binding = [],
-           typ = if null instT then [] else [Term_Subst.instantiateT instT],
+           typ =
+            if Term_Subst.TVars.is_empty instT then []
+            else [Term_Subst.instantiateT instT],
            term = [Term_Subst.instantiate (instT, inst)],
            fact = [map (Thm.instantiate (cinstT, cinst))]}
       end;
diff -r 1d25be2353e1 -r c49134ee16c1 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/proofterm.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -114,8 +114,7 @@
   val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof
   val permute_prems_proof: term list -> int -> int -> proof -> proof
   val generalize_proof: Symtab.set * Symtab.set -> int -> term -> proof -> proof
-  val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
-    -> proof -> proof
+  val instantiate: typ Term_Subst.TVars.table * term Term_Subst.Vars.table -> proof -> proof
   val lift_proof: term -> int -> term -> proof -> proof
   val incr_indexes: int -> proof -> proof
   val assumption_proof: term list -> term -> int -> proof -> proof
@@ -672,18 +671,25 @@
 
 (* substitutions *)
 
-fun del_conflicting_tvars envT T = Term_Subst.instantiateT
-  (map_filter (fn ixnS as (_, S) =>
-     (Type.lookup envT ixnS; NONE) handle TYPE _ =>
-        SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvarsT T [])) T;
+fun del_conflicting_tvars envT T =
+  let
+    val instT =
+      map_filter (fn ixnS as (_, S) =>
+        (Type.lookup envT ixnS; NONE) handle TYPE _ =>
+          SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvarsT T [])
+  in Term_Subst.instantiateT (Term_Subst.TVars.table instT) T end;
 
-fun del_conflicting_vars env t = Term_Subst.instantiate
-  (map_filter (fn ixnS as (_, S) =>
-     (Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
-        SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvars t []),
-   map_filter (fn (ixnT as (_, T)) =>
-     (Envir.lookup env ixnT; NONE) handle TYPE _ =>
-        SOME (ixnT, Free ("dummy", T))) (Term.add_vars t [])) t;
+fun del_conflicting_vars env t =
+  let
+    val instT =
+      map_filter (fn ixnS as (_, S) =>
+        (Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ =>
+          SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvars t []);
+    val inst =
+      map_filter (fn (ixnT as (_, T)) =>
+        (Envir.lookup env ixnT; NONE) handle TYPE _ =>
+          SOME (ixnT, Free ("dummy", T))) (Term.add_vars t []);
+  in Term_Subst.instantiate (Term_Subst.TVars.make instT, Term_Subst.Vars.table inst) t end;
 
 fun norm_proof env =
   let
@@ -967,7 +973,7 @@
 
 fun instantiate (instT, inst) =
   Same.commit (map_proof_terms_same
-    (Term_Subst.instantiate_same (instT, map (apsnd remove_types) inst))
+    (Term_Subst.instantiate_same (instT, Term_Subst.Vars.map (K remove_types) inst))
     (Term_Subst.instantiateT_same instT));
 
 
diff -r 1d25be2353e1 -r c49134ee16c1 src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/term_subst.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -4,8 +4,31 @@
 Efficient type/term substitution.
 *)
 
+signature INST_TABLE =
+sig
+  include TABLE
+  val add: key * 'a -> 'a table -> 'a table
+  val table: (key * 'a) list -> 'a table
+end;
+
+functor Inst_Table(Key: KEY): INST_TABLE =
+struct
+
+structure Tab = Table(Key);
+
+fun add entry = Tab.insert (K true) entry;
+fun table entries = fold add entries Tab.empty;
+
+open Tab;
+
+end;
+
 signature TERM_SUBST =
 sig
+  structure TFrees: INST_TABLE
+  structure TVars: INST_TABLE
+  structure Frees: INST_TABLE
+  structure Vars: INST_TABLE
   val map_atypsT_same: typ Same.operation -> typ Same.operation
   val map_types_same: typ Same.operation -> term Same.operation
   val map_aterms_same: term Same.operation -> term Same.operation
@@ -13,24 +36,18 @@
   val generalize_same: Symtab.set * Symtab.set -> int -> term Same.operation
   val generalizeT: Symtab.set -> int -> typ -> typ
   val generalize: Symtab.set * Symtab.set -> int -> term -> term
-  val instantiateT_maxidx: ((indexname * sort) * (typ * int)) list -> typ -> int -> typ * int
-  val instantiate_maxidx:
-    ((indexname * sort) * (typ * int)) list * ((indexname * typ) * (term * int)) list ->
+  val instantiateT_maxidx: (typ * int) TVars.table -> typ -> int -> typ * int
+  val instantiate_maxidx: (typ * int) TVars.table * (term * int) Vars.table ->
     term -> int -> term * int
-  val instantiateT_frees_same: ((string * sort) * typ) list -> typ Same.operation
-  val instantiate_frees_same: ((string * sort) * typ) list * ((string * typ) * term) list ->
-    term Same.operation
-  val instantiateT_frees: ((string * sort) * typ) list -> typ -> typ
-  val instantiate_frees: ((string * sort) * typ) list * ((string * typ) * term) list ->
-    term -> term
-  val instantiateT_same: ((indexname * sort) * typ) list -> typ Same.operation
-  val instantiate_same: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
-    term Same.operation
-  val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
-  val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
-    term -> term
-  val zero_var_indexes_inst: Name.context -> term list ->
-    ((indexname * sort) * typ) list * ((indexname * typ) * term) list
+  val instantiateT_frees_same: typ TFrees.table -> typ Same.operation
+  val instantiate_frees_same: typ TFrees.table * term Frees.table -> term Same.operation
+  val instantiateT_frees: typ TFrees.table -> typ -> typ
+  val instantiate_frees: typ TFrees.table * term Frees.table -> term -> term
+  val instantiateT_same: typ TVars.table -> typ Same.operation
+  val instantiate_same: typ TVars.table * term Vars.table -> term Same.operation
+  val instantiateT: typ TVars.table -> typ -> typ
+  val instantiate: typ TVars.table * term Vars.table -> term -> term
+  val zero_var_indexes_inst: Name.context -> term list -> typ TVars.table * term Vars.table
   val zero_var_indexes: term -> term
   val zero_var_indexes_list: term list -> term list
 end;
@@ -38,6 +55,29 @@
 structure Term_Subst: TERM_SUBST =
 struct
 
+(* instantiation as table *)
+
+structure TFrees = Inst_Table(
+  type key = string * sort
+  val ord = prod_ord fast_string_ord Term_Ord.sort_ord
+);
+
+structure TVars = Inst_Table(
+  type key = indexname * sort
+  val ord = prod_ord Term_Ord.fast_indexname_ord Term_Ord.sort_ord
+);
+
+structure Frees = Inst_Table(
+  type key = string * typ
+  val ord = prod_ord fast_string_ord Term_Ord.typ_ord
+);
+
+structure Vars = Inst_Table(
+  type key = indexname * typ
+  val ord = prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord
+);
+
+
 (* generic mapping *)
 
 fun map_atypsT_same f =
@@ -103,35 +143,37 @@
 
 (* instantiation of free variables (types before terms) *)
 
-fun instantiateT_frees_same [] _ = raise Same.SAME
-  | instantiateT_frees_same instT ty =
-      let
-        fun subst (Type (a, Ts)) = Type (a, Same.map subst Ts)
-          | subst (TFree v) =
-              (case AList.lookup (op =) instT v of
-                SOME T => T
-              | NONE => raise Same.SAME)
-          | subst _ = raise Same.SAME;
-      in subst ty end;
+fun instantiateT_frees_same instT ty =
+  if TFrees.is_empty instT then raise Same.SAME
+  else
+    let
+      fun subst (Type (a, Ts)) = Type (a, Same.map subst Ts)
+        | subst (TFree v) =
+            (case TFrees.lookup instT v of
+              SOME T => T
+            | NONE => raise Same.SAME)
+        | subst _ = raise Same.SAME;
+    in subst ty end;
 
-fun instantiate_frees_same ([], []) _ = raise Same.SAME
-  | instantiate_frees_same (instT, inst) tm =
-      let
-        val substT = instantiateT_frees_same instT;
-        fun subst (Const (c, T)) = Const (c, substT T)
-          | subst (Free (x, T)) =
-              let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
-                (case AList.lookup (op =) inst (x, T') of
-                   SOME t => t
-                 | NONE => if same then raise Same.SAME else Free (x, T'))
-              end
-          | subst (Var (xi, T)) = Var (xi, substT T)
-          | subst (Bound _) = raise Same.SAME
-          | subst (Abs (x, T, t)) =
-              (Abs (x, substT T, Same.commit subst t)
-                handle Same.SAME => Abs (x, T, subst t))
-          | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
-      in subst tm end;
+fun instantiate_frees_same (instT, inst) tm =
+  if TFrees.is_empty instT andalso Frees.is_empty inst then raise Same.SAME
+  else
+    let
+      val substT = instantiateT_frees_same instT;
+      fun subst (Const (c, T)) = Const (c, substT T)
+        | subst (Free (x, T)) =
+            let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
+              (case Frees.lookup inst (x, T') of
+                 SOME t => t
+               | NONE => if same then raise Same.SAME else Free (x, T'))
+            end
+        | subst (Var (xi, T)) = Var (xi, substT T)
+        | subst (Bound _) = raise Same.SAME
+        | subst (Abs (x, T, t)) =
+            (Abs (x, substT T, Same.commit subst t)
+              handle Same.SAME => Abs (x, T, subst t))
+        | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
+    in subst tm end;
 
 fun instantiateT_frees instT ty = Same.commit (instantiateT_frees_same instT) ty;
 fun instantiate_frees inst tm = Same.commit (instantiate_frees_same inst) tm;
@@ -141,9 +183,8 @@
 
 local
 
-fun no_index (x, y) = (x, (y, ~1));
-fun no_indexes1 inst = map no_index inst;
-fun no_indexes2 (inst1, inst2) = (map no_index inst1, map no_index inst2);
+fun no_indexesT instT = TVars.map (fn _ => rpair ~1) instT;
+fun no_indexes inst = Vars.map (fn _ => rpair ~1) inst;
 
 fun instT_same maxidx instT ty =
   let
@@ -151,7 +192,7 @@
 
     fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
       | subst_typ (TVar ((a, i), S)) =
-          (case AList.lookup Term.eq_tvar instT ((a, i), S) of
+          (case TVars.lookup instT ((a, i), S) of
             SOME (T, j) => (maxify j; T)
           | NONE => (maxify i; raise Same.SAME))
       | subst_typ _ = raise Same.SAME
@@ -170,7 +211,7 @@
       | subst (Free (x, T)) = Free (x, substT T)
       | subst (Var ((x, i), T)) =
           let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
-            (case AList.lookup Term.eq_var inst ((x, i), T') of
+            (case Vars.lookup inst ((x, i), T') of
                SOME (t, j) => (maxify j; t)
              | NONE => (maxify i; if same then raise Same.SAME else Var ((x, i), T')))
           end
@@ -191,11 +232,13 @@
   let val maxidx = Unsynchronized.ref i
   in (Same.commit (inst_same maxidx insts) tm, ! maxidx) end;
 
-fun instantiateT_same [] _ = raise Same.SAME
-  | instantiateT_same instT ty = instT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty;
+fun instantiateT_same instT ty =
+  if TVars.is_empty instT then raise Same.SAME
+  else instT_same (Unsynchronized.ref ~1) (no_indexesT instT) ty;
 
-fun instantiate_same ([], []) _ = raise Same.SAME
-  | instantiate_same insts tm = inst_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm;
+fun instantiate_same (instT, inst) tm =
+  if TVars.is_empty instT andalso Vars.is_empty inst then raise Same.SAME
+  else inst_same (Unsynchronized.ref ~1) (no_indexesT instT, no_indexes inst) tm;
 
 fun instantiateT instT ty = Same.commit (instantiateT_same instT) ty;
 fun instantiate inst tm = Same.commit (instantiate_same inst) tm;
@@ -205,26 +248,20 @@
 
 (* zero var indexes *)
 
-structure TVars = Table(type key = indexname * sort val ord = Term_Ord.tvar_ord);
-structure Vars = Table(type key = indexname * typ val ord = Term_Ord.var_ord);
-
-fun zero_var_inst mk (v as ((x, i), X)) (inst, used) =
-  let
-    val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used;
-  in if x = x' andalso i = 0 then (inst, used') else ((v, mk ((x', 0), X)) :: inst, used') end;
+fun zero_var_inst ins mk (v as ((x, i), X)) (inst, used) =
+  let val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used
+  in if x = x' andalso i = 0 then (inst, used') else (ins (v, mk ((x', 0), X)) inst, used') end;
 
 fun zero_var_indexes_inst used ts =
   let
     val (instT, _) =
-      TVars.fold (zero_var_inst TVar o #1)
+      (TVars.empty, used) |> TVars.fold (zero_var_inst TVars.add TVar o #1)
         ((fold o fold_types o fold_atyps) (fn TVar v =>
-          TVars.insert (K true) (v, ()) | _ => I) ts TVars.empty)
-        ([], used);
+          TVars.add (v, ()) | _ => I) ts TVars.empty);
     val (inst, _) =
-      Vars.fold (zero_var_inst Var o #1)
+      (Vars.empty, used) |> Vars.fold (zero_var_inst Vars.add Var o #1)
         ((fold o fold_aterms) (fn Var (xi, T) =>
-          Vars.insert (K true) ((xi, instantiateT instT T), ()) | _ => I) ts Vars.empty)
-        ([], used);
+          Vars.add ((xi, instantiateT instT T), ()) | _ => I) ts Vars.empty);
   in (instT, inst) end;
 
 fun zero_var_indexes_list ts = map (instantiate (zero_var_indexes_inst Name.context ts)) ts;
diff -r 1d25be2353e1 -r c49134ee16c1 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/thm.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -1611,12 +1611,12 @@
 val add_instT_sorts = add_sorts (fn Ctyp {sorts, ...} => sorts);
 val add_inst_sorts = add_sorts (fn Cterm {sorts, ...} => sorts);
 
-fun make_instT thy (v as (_, S), Ctyp {T = U, maxidx, ...}) =
-  if Sign.of_sort thy (U, S) then (v, (U, maxidx))
+fun add_instT thy (v as (_, S), Ctyp {T = U, maxidx, ...}) =
+  if Sign.of_sort thy (U, S) then Term_Subst.TVars.add (v, (U, maxidx))
   else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy S, [U], []);
 
-fun make_inst thy (v as (_, T), Cterm {t = u, T = U, maxidx, ...}) =
-  if T = U then (v, (u, maxidx))
+fun add_inst thy (v as (_, T), Cterm {t = u, T = U, maxidx, ...}) =
+  if T = U then Term_Subst.Vars.add (v, (u, maxidx))
   else
     let
       fun pretty_typing t ty =
@@ -1641,8 +1641,8 @@
       |> fold add_instT_sorts instT
       |> fold add_inst_sorts inst;
 
-    val instT' = map (make_instT thy') instT;
-    val inst' = map (make_inst thy') inst;
+    val instT' = fold (add_instT thy') instT Term_Subst.TVars.empty;
+    val inst' = fold (add_inst thy') inst Term_Subst.Vars.empty;
   in ((instT', inst'), (cert', sorts')) end;
 
 in
@@ -1665,10 +1665,13 @@
 
         val thy' = Context.certificate_theory cert';
         val constraints' =
-          fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S)) instT' constraints;
+          Term_Subst.TVars.fold (fn ((_, S), (T, _)) => insert_constraints thy' (T, S))
+            instT' constraints;
       in
         Thm (deriv_rule1
-          (fn d => Proofterm.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der,
+          (fn d =>
+            Proofterm.instantiate
+              (Term_Subst.TVars.map (K #1) instT', Term_Subst.Vars.map (K #1) inst') d) der,
          {cert = cert',
           tags = [],
           maxidx = maxidx',
diff -r 1d25be2353e1 -r c49134ee16c1 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/type_infer.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -114,10 +114,10 @@
         let
           val [a] = Name.invent used Name.aT 1;
           val used' = Name.declare a used;
-        in (((xi, S), TFree (a, improve_sort S)) :: inst, used') end
+        in (Term_Subst.TVars.add ((xi, S), TFree (a, improve_sort S)) inst, used') end
       else (inst, used);
     val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
-    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
+    val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) (Term_Subst.TVars.empty, used);
   in (map o map_types) (Term_Subst.instantiateT inst) ts end;
 
 end;
diff -r 1d25be2353e1 -r c49134ee16c1 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Fri Sep 03 14:34:14 2021 +0200
+++ b/src/Pure/variable.ML	Fri Sep 03 18:57:33 2021 +0200
@@ -69,9 +69,9 @@
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_morphism: Proof.context -> Proof.context -> morphism
   val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
-  val importT_inst: term list -> Proof.context -> ((indexname * sort) * typ) list * Proof.context
+  val importT_inst: term list -> Proof.context -> typ Term_Subst.TVars.table * Proof.context
   val import_inst: bool -> term list -> Proof.context ->
-    (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
+    (typ Term_Subst.TVars.table * term Term_Subst.Vars.table) * Proof.context
   val importT_terms: term list -> Proof.context -> term list * Proof.context
   val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
   val importT: thm list -> Proof.context ->
@@ -593,20 +593,25 @@
   let
     val tvars = rev (fold Term.add_tvars ts []);
     val (tfrees, ctxt') = invent_types (map #2 tvars) ctxt;
-  in (tvars ~~ map TFree tfrees, ctxt') end;
+    val instT =
+      fold2 (fn a => fn b => Term_Subst.TVars.add (a, TFree b))
+        tvars tfrees Term_Subst.TVars.empty;
+  in (instT, ctxt') end;
 
 fun import_inst is_open ts ctxt =
   let
     val ren = Name.clean #> (if is_open then I else Name.internal);
     val (instT, ctxt') = importT_inst ts ctxt;
     val vars = map (apsnd (Term_Subst.instantiateT instT)) (rev (fold Term.add_vars ts []));
-    val (xs, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';
-    val inst = vars ~~ map Free (xs ~~ map #2 vars);
+    val (ys, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';
+    val inst =
+      fold2 (fn (x, T) => fn y => Term_Subst.Vars.add ((x, T), Free (y, T)))
+        vars ys Term_Subst.Vars.empty;
   in ((instT, inst), ctxt'') end;
 
 fun importT_terms ts ctxt =
   let val (instT, ctxt') = importT_inst ts ctxt
-  in (map (Term_Subst.instantiate (instT, [])) ts, ctxt') end;
+  in (map (Term_Subst.instantiate (instT, Term_Subst.Vars.empty)) ts, ctxt') end;
 
 fun import_terms is_open ts ctxt =
   let val (inst, ctxt') = import_inst is_open ts ctxt
@@ -615,7 +620,7 @@
 fun importT ths ctxt =
   let
     val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
-    val instT' = map (apsnd (Thm.ctyp_of ctxt')) instT;
+    val instT' = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T)) instT [];
     val ths' = map (Thm.instantiate (instT', [])) ths;
   in ((instT', ths'), ctxt') end;
 
@@ -628,11 +633,10 @@
 fun import is_open ths ctxt =
   let
     val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;
-    val insts' =
-     (map (apsnd (Thm.ctyp_of ctxt')) instT,
-      map (apsnd (Thm.cterm_of ctxt')) inst);
-    val ths' = map (Thm.instantiate insts') ths;
-  in ((insts', ths'), ctxt') end;
+    val instT' = Term_Subst.TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt' T)) instT [];
+    val inst' = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt' t)) inst [];
+    val ths' = map (Thm.instantiate (instT', inst')) ths;
+  in (((instT', inst'), ths'), ctxt') end;
 
 fun import_vars ctxt th =
   let val ((_, [th']), _) = ctxt |> set_body false |> import true [th];