more scalable operations;

--- a/src/Pure/drule.ML	Mon Sep 06 11:39:44 2021 +0200
+++ b/src/Pure/drule.ML	Mon Sep 06 11:55:54 2021 +0200
@@ -165,7 +165,12 @@
 val forall_intr_list = fold_rev Thm.forall_intr;
 
 (*Generalization over Vars -- canonical order*)
-fun forall_intr_vars th = fold Thm.forall_intr (Thm.add_vars th []) th;
+fun forall_intr_vars th =
+  let
+    val vs =
+      build (th |> Thm.fold_atomic_cterms {hyps = false} (fn a =>
+        is_Var (Thm.term_of a) ? insert (op aconvc) a));
+  in fold Thm.forall_intr vs th end;
 
 fun outer_params t =
   let val vs = Term.strip_all_vars t
@@ -218,14 +223,14 @@
         val (instT, inst) =
           Term_Subst.zero_var_indexes_inst Name.context (map Thm.full_prop_of ths);
 
-        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 tvars = fold Thm.add_tvars ths Term_Subst.TVars.empty;
+        val the_tvar = the o Term_Subst.TVars.lookup tvars;
         val instT' =
           build (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 vars = fold (Thm.add_vars o Thm.instantiate (instT', [])) ths Term_Subst.Vars.empty;
+        val the_var = the o Term_Subst.Vars.lookup vars;
         val inst' =
           build (inst |> Term_Subst.Vars.fold (fn (v, Var (b, _)) =>
             cons (v, Thm.var (b, Thm.ctyp_of_cterm (the_var v)))));

--- a/src/Pure/more_thm.ML	Mon Sep 06 11:39:44 2021 +0200
+++ b/src/Pure/more_thm.ML	Mon Sep 06 11:55:54 2021 +0200
@@ -25,8 +25,8 @@
   structure Thmtab: TABLE
   val eq_ctyp: ctyp * ctyp -> bool
   val aconvc: cterm * cterm -> bool
-  val add_tvars: thm -> ctyp list -> ctyp list
-  val add_vars: thm -> cterm list -> cterm list
+  val add_tvars: thm -> ctyp Term_Subst.TVars.table -> ctyp Term_Subst.TVars.table
+  val add_vars: thm -> cterm Term_Subst.Vars.table -> cterm Term_Subst.Vars.table
   val frees_of: thm -> cterm list
   val dest_funT: ctyp -> ctyp * ctyp
   val strip_type: ctyp -> ctyp list * ctyp
@@ -138,9 +138,22 @@
 val op aconvc = op aconv o apply2 Thm.term_of;
 
 val add_tvars =
-  Thm.fold_atomic_ctyps {hyps = false} (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a);
+  Thm.fold_atomic_ctyps {hyps = false} (fn cT => fn tab =>
+    (case Thm.typ_of cT of
+      TVar v =>
+        if not (Term_Subst.TVars.defined tab v)
+        then Term_Subst.TVars.update (v, cT) tab
+        else tab
+    | _ => tab));
+
 val add_vars =
-  Thm.fold_atomic_cterms {hyps = false} (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a);
+  Thm.fold_atomic_cterms {hyps = false} (fn ct => fn tab =>
+    (case Thm.term_of ct of
+      Var v =>
+        if not (Term_Subst.Vars.defined tab v)
+        then Term_Subst.Vars.update (v, ct) tab
+        else tab
+    | _ => tab));
 
 fun frees_of th =
   (th, (Term_Subst.Frees.empty, [])) |-> Thm.fold_atomic_cterms {hyps = true}