--- 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
--- 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 =>
--- 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
--- 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);
--- 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, ...})) =
--- 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));
--- 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;