# HG changeset patch
# User wenzelm
# Date 1630757924 -7200
# Node ID c22e5bdb207d5f84d03d9ad74bcdf453a44b2c0a
# Parent  fdcc7e8f95ea34152854c8ceb9aa808a1b882337
more scalable operations;
tuned;

diff -r fdcc7e8f95ea -r c22e5bdb207d src/Pure/Proof/proof_checker.ML
--- a/src/Pure/Proof/proof_checker.ML	Sat Sep 04 13:49:26 2021 +0200
+++ b/src/Pure/Proof/proof_checker.ML	Sat Sep 04 14:18:44 2021 +0200
@@ -76,7 +76,7 @@
 
         fun thm_of_atom thm Ts =
           let
-            val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
+            val tvars = rev (Term.add_tvars (Thm.full_prop_of thm) []);
             val (fmap, thm') = Thm.varifyT_global' [] thm;
             val ctye =
               (tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts);
diff -r fdcc7e8f95ea -r c22e5bdb207d src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Sat Sep 04 13:49:26 2021 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Sat Sep 04 14:18:44 2021 +0200
@@ -249,7 +249,7 @@
           if member (op =) defs s then
             let
               val vs = vars_of prop;
-              val tvars = Term.add_tvars prop [] |> rev;
+              val tvars = rev (Term.add_tvars prop []);
               val (_, rhs) = Logic.dest_equals (Logic.strip_imp_concl prop);
               val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
                 (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
@@ -291,11 +291,11 @@
 fun elim_vars mk_default prf =
   let
     val prop = Proofterm.prop_of prf;
-    val tv = Term.add_vars prop [];
-    val tf = Term.add_frees prop [];
+    val tv = Term_Subst.add_vars prop Term_Subst.Vars.empty;
+    val tf = Term_Subst.add_frees prop Term_Subst.Frees.empty;
 
-    fun hidden_variable (Var v) = not (member (op =) tv v)
-      | hidden_variable (Free f) = not (member (op =) tf f)
+    fun hidden_variable (Var v) = not (Term_Subst.Vars.defined tv v)
+      | hidden_variable (Free f) = not (Term_Subst.Frees.defined tf f)
       | hidden_variable _ = false;
 
     fun mk_default' T =
@@ -303,8 +303,8 @@
 
     fun elim_varst (t $ u) = elim_varst t $ elim_varst u
       | elim_varst (Abs (s, T, t)) = Abs (s, T, elim_varst t)
-      | elim_varst (t as Free (x, T)) = if member (op =) tf (x, T) then t else mk_default' T
-      | elim_varst (t as Var (xi, T)) = if member (op =) tv (xi, T) then t else mk_default' T
+      | elim_varst (t as Free (x, T)) = if Term_Subst.Frees.defined tf (x, T) then t else mk_default' T
+      | elim_varst (t as Var (xi, T)) = if Term_Subst.Vars.defined tv (xi, T) then t else mk_default' T
       | elim_varst t = t;
   in
     Proofterm.map_proof_terms (fn t =>
diff -r fdcc7e8f95ea -r c22e5bdb207d src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Sep 04 13:49:26 2021 +0200
+++ b/src/Pure/proofterm.ML	Sat Sep 04 14:18:44 2021 +0200
@@ -671,25 +671,36 @@
 
 (* substitutions *)
 
-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;
+local
+
+fun conflicting_tvarsT envT =
+  Term.fold_atyps
+    (fn T => fn instT =>
+      (case T of
+        TVar (v as (_, S)) =>
+          if Term_Subst.TVars.defined instT v orelse can (Type.lookup envT) v then instT
+          else Term_Subst.TVars.update (v, Logic.dummy_tfree S) instT
+      | _ => instT));
 
-fun del_conflicting_vars env t =
+fun conflicting_tvars env =
+  Term.fold_aterms
+    (fn t => fn inst =>
+      (case t of
+        Var (v as (_, T)) =>
+          if Term_Subst.Vars.defined inst v orelse can (Envir.lookup env) v then inst
+          else Term_Subst.Vars.update (v, Free ("dummy", T)) inst
+      | _ => inst));
+
+fun del_conflicting_tvars envT ty =
+  Term_Subst.instantiateT (conflicting_tvarsT envT ty Term_Subst.TVars.empty) ty;
+
+fun del_conflicting_vars env tm =
   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;
+    val instT = Term.fold_types (conflicting_tvarsT (Envir.type_env env)) tm Term_Subst.TVars.empty;
+    val inst = conflicting_tvars env tm Term_Subst.Vars.empty;
+  in Term_Subst.instantiate (instT, inst) tm end;
+
+in
 
 fun norm_proof env =
   let
@@ -726,6 +737,8 @@
       | norm _ = raise Same.SAME;
   in Same.commit norm end;
 
+end;
+
 
 (* remove some types in proof term (to save space) *)