# HG changeset patch
# User wenzelm
# Date 1630784743 -7200
# Node ID 9eff7c673b42cc996a2789fcb2e1edceaea95636
# Parent  1091880266e5088b17a839cebe12bf0db1541f15
more scalable operations;

diff -r 1091880266e5 -r 9eff7c673b42 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Sep 04 21:25:08 2021 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Sat Sep 04 21:45:43 2021 +0200
@@ -1162,7 +1162,9 @@
   let
      val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
      fun varify (t, (i, ts)) =
-       let val t' = map_types (Logic.incr_tvar (i + 1)) (#2 (Type.varify_global [] t))
+       let
+         val t' = map_types (Logic.incr_tvar (i + 1))
+           (#2 (Type.varify_global Term_Subst.TFrees.empty t))
        in (maxidx_of_term t', t' :: ts) end
      val (i, cs') = List.foldr varify (~1, []) cs
      val (i', intr_ts') = List.foldr varify (i, []) intr_ts
diff -r 1091880266e5 -r 9eff7c673b42 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sat Sep 04 21:25:08 2021 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Sat Sep 04 21:45:43 2021 +0200
@@ -99,7 +99,7 @@
     val frees = map snd props''
     val prop = myfoldr HOLogic.mk_conj (map fst props'')
 
-    val (vmap, prop_thawed) = Type.varify_global [] prop
+    val (vmap, prop_thawed) = Type.varify_global Term_Subst.TFrees.empty prop
     val thawed_prop_consts = collect_consts (prop_thawed, [])
     val (altcos, overloaded) = split_list cos
     val (names, sconsts) = split_list altcos
@@ -109,7 +109,7 @@
 
     fun proc_const c =
       let
-        val (_, c') = Type.varify_global [] c
+        val (_, c') = Type.varify_global Term_Subst.TFrees.empty c
         val (cname,ctyp) = dest_Const c'
       in
         (case filter (fn t =>
diff -r 1091880266e5 -r 9eff7c673b42 src/Pure/Proof/proof_checker.ML
--- a/src/Pure/Proof/proof_checker.ML	Sat Sep 04 21:25:08 2021 +0200
+++ b/src/Pure/Proof/proof_checker.ML	Sat Sep 04 21:45:43 2021 +0200
@@ -77,7 +77,7 @@
         fun thm_of_atom thm Ts =
           let
             val tvars = rev (Term.add_tvars (Thm.full_prop_of thm) []);
-            val (fmap, thm') = Thm.varifyT_global' [] thm;
+            val (fmap, thm') = Thm.varifyT_global' Term_Subst.TFrees.empty thm;
             val ctye =
               (tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts);
           in
diff -r 1091880266e5 -r 9eff7c673b42 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Sep 04 21:25:08 2021 +0200
+++ b/src/Pure/proofterm.ML	Sat Sep 04 21:45:43 2021 +0200
@@ -109,7 +109,7 @@
   val implies_intr_proof': term -> proof -> proof
   val forall_intr_proof: string * term -> typ option -> proof -> proof
   val forall_intr_proof': term -> proof -> proof
-  val varify_proof: term -> (string * sort) list -> proof -> proof
+  val varify_proof: term -> Term_Subst.TFrees.set -> proof -> proof
   val legacy_freezeT: term -> proof -> proof
   val rotate_proof: term list -> term -> (string * typ) list -> term list -> int -> proof -> proof
   val permute_prems_proof: term list -> int -> int -> proof -> proof
@@ -901,8 +901,9 @@
 
 fun varify_proof t fixed prf =
   let
-    val fs = Term.fold_types (Term.fold_atyps
-      (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
+    val fs =
+      (t, []) |-> (Term.fold_types o Term.fold_atyps)
+        (fn TFree v => if Term_Subst.TFrees.defined fixed v then I else insert (op =) v | _ => I);
     val used = Name.context
       |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
     val fmap = fs ~~ #1 (fold_map Name.variant (map fst fs) used);
diff -r 1091880266e5 -r 9eff7c673b42 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Sep 04 21:25:08 2021 +0200
+++ b/src/Pure/thm.ML	Sat Sep 04 21:45:43 2021 +0200
@@ -161,7 +161,7 @@
   val trivial: cterm -> thm
   val of_class: ctyp * class -> thm
   val unconstrainT: thm -> thm
-  val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
+  val varifyT_global': Term_Subst.TFrees.set -> thm -> ((string * sort) * indexname) list * thm
   val varifyT_global: thm -> thm
   val legacy_freezeT: thm -> thm
   val plain_prop_of: thm -> term
@@ -1776,7 +1776,7 @@
 (*Replace all TFrees not fixed or in the hyps by new TVars*)
 fun varifyT_global' fixed (Thm (der, {cert, maxidx, constraints, shyps, hyps, tpairs, prop, ...})) =
   let
-    val tfrees = fold Term.add_tfrees hyps fixed;
+    val tfrees = fold Term_Subst.add_tfrees hyps fixed;
     val prop1 = attach_tpairs tpairs prop;
     val (al, prop2) = Type.varify_global tfrees prop1;
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
@@ -1792,7 +1792,7 @@
       prop = prop3}))
   end;
 
-val varifyT_global = #2 o varifyT_global' [];
+val varifyT_global = #2 o varifyT_global' Term_Subst.TFrees.empty;
 
 (*Replace all TVars by TFrees that are often new*)
 fun legacy_freezeT (Thm (der, {cert, constraints, shyps, hyps, tpairs, prop, ...})) =
diff -r 1091880266e5 -r 9eff7c673b42 src/Pure/type.ML
--- a/src/Pure/type.ML	Sat Sep 04 21:25:08 2021 +0200
+++ b/src/Pure/type.ML	Sat Sep 04 21:45:43 2021 +0200
@@ -61,7 +61,7 @@
   val strip_sorts: typ -> typ
   val strip_sorts_dummy: typ -> typ
   val no_tvars: typ -> typ
-  val varify_global: (string * sort) list -> term -> ((string * sort) * indexname) list * term
+  val varify_global: Term_Subst.TFrees.set -> term -> ((string * sort) * indexname) list * term
   val legacy_freeze_thaw_type: typ -> typ * (typ -> typ)
   val legacy_freeze_type: typ -> typ
   val legacy_freeze_thaw: term -> term * (term -> term)
@@ -355,8 +355,9 @@
 
 fun varify_global fixed t =
   let
-    val fs = Term.fold_types (Term.fold_atyps
-      (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
+    val fs =
+      (t, []) |-> (Term.fold_types o Term.fold_atyps)
+        (fn TFree v => if Term_Subst.TFrees.defined fixed v then I else insert (op =) v | _ => I);
     val used = Name.context
       |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
     val fmap = fs ~~ map (rpair 0) (#1 (fold_map Name.variant (map fst fs) used));
diff -r 1091880266e5 -r 9eff7c673b42 src/Tools/IsaPlanner/rw_inst.ML
--- a/src/Tools/IsaPlanner/rw_inst.ML	Sat Sep 04 21:25:08 2021 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Sat Sep 04 21:45:43 2021 +0200
@@ -236,7 +236,7 @@
     |> Drule.implies_intr_list cprems
     |> Drule.forall_intr_list frees_of_fixed_vars
     |> Drule.forall_elim_list vars
-    |> Thm.varifyT_global' othertfrees
+    |> Thm.varifyT_global' (Term_Subst.TFrees.make_set othertfrees)
     |-> K Drule.zero_var_indexes
   end;