--- 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);
--- 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 =>
--- 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) *)