# HG changeset patch
# User wenzelm
# Date 1721508207 -7200
# Node ID 9efbbad0a83450a136d85395a61e7db9fd251f27
# Parent  1effd04264ccc571794657176e3ad5bf96085224# Parent  f8c070249502011e3a023bdcb15785ed8055b6b3
merged

diff -r 1effd04264cc -r 9efbbad0a834 src/Pure/name.ML
--- a/src/Pure/name.ML	Sat Jul 20 16:47:04 2024 +0100
+++ b/src/Pure/name.ML	Sat Jul 20 22:43:27 2024 +0200
@@ -31,6 +31,7 @@
   val invent_names: context -> string -> 'a list -> (string * 'a) list
   val invent_list: string list -> string -> int -> string list
   val variant: string -> context -> string * context
+  val variant_bound: string -> context -> string * context
   val variant_list: string list -> string list -> string list
   val enforce_case: bool -> string -> string
   val desymbolize: bool option -> string -> string
@@ -150,6 +151,8 @@
         in (x', ctxt') end;
   in (x' ^ replicate_string n "_", ctxt') end;
 
+fun variant_bound name = variant (if is_bound name then "u" else name);
+
 fun variant_list used names = #1 (make_context used |> fold_map variant names);
 
 
diff -r 1effd04264cc -r 9efbbad0a834 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Jul 20 16:47:04 2024 +0100
+++ b/src/Pure/proofterm.ML	Sat Jul 20 22:43:27 2024 +0200
@@ -2038,31 +2038,28 @@
 
 local
 
-val declare_names_term = Term.declare_term_frees;
-val declare_names_term' = fn SOME t => declare_names_term t | NONE => I;
-val declare_names_proof = fold_proof_terms declare_names_term;
-
-fun variant names bs x =
-  #1 (Name.variant x (fold Name.declare bs names));
+val declare_frees_term = Term.declare_term_frees;
+val declare_frees_term' = fn SOME t => declare_frees_term t | NONE => I;
+val declare_frees_proof = fold_proof_terms declare_frees_term;
 
 fun variant_term bs (Abs (x, T, t)) =
       let
-        val x' = variant (declare_names_term t Name.context) bs x;
-        val t' = variant_term (x' :: bs) t;
+        val x' = #1 (Name.variant x (declare_frees_term t bs));
+        val t' = variant_term (Name.declare x' bs) t;
       in Abs (x', T, t') end
   | variant_term bs (t $ u) = variant_term bs t $ variant_term bs u
   | variant_term _ t = t;
 
 fun variant_proof bs (Abst (x, T, prf)) =
       let
-        val x' = variant (declare_names_proof prf Name.context) bs x;
-        val prf' = variant_proof (x' :: bs) prf;
+        val x' = #1 (Name.variant x (declare_frees_proof prf bs));
+        val prf' = variant_proof (Name.declare x' bs) prf;
       in Abst (x', T, prf') end
   | variant_proof bs (AbsP (x, t, prf)) =
       let
-        val x' = variant (declare_names_term' t (declare_names_proof prf Name.context)) bs x;
+        val x' = #1 (Name.variant x (declare_frees_term' t (declare_frees_proof prf bs)));
         val t' = Option.map (variant_term bs) t;
-        val prf' = variant_proof (x' :: bs) prf;
+        val prf' = variant_proof (Name.declare x' bs) prf;
       in AbsP (x', t', prf') end
   | variant_proof bs (prf % t) = variant_proof bs prf % Option.map (variant_term bs) t
   | variant_proof bs (prf1 %% prf2) = variant_proof bs prf1 %% variant_proof bs prf2
@@ -2070,12 +2067,12 @@
   | variant_proof _ prf = prf;
 
 val used_frees_type = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
-fun used_frees_term t = fold_types used_frees_type t #> Term.declare_term_frees t;
+fun used_frees_term t = fold_types used_frees_type t #> declare_frees_term t;
 val used_frees_proof = fold_proof_terms_types used_frees_term used_frees_type;
 
-val unvarifyT = Term.map_atyps (fn TVar ((a, _), S) => TFree (a, S) | T => T);
-val unvarify = Term.map_aterms (fn Var ((x, _), T) => Free (x, T) | t => t) #> map_types unvarifyT;
-val unvarify_proof = map_proof_terms unvarify unvarifyT;
+val unvarify_type = Term.map_atyps (fn TVar ((a, _), S) => TFree (a, S) | T => T);
+val unvarify_term = map_types unvarify_type o Term.map_aterms (fn Var ((x, _), T) => Free (x, T) | t => t);
+val unvarify_proof = map_proof_terms unvarify_term unvarify_type;
 
 fun hidden_types prop proof =
   let
@@ -2083,10 +2080,10 @@
     val add_hiddenT = fold_atyps (fn T => not (member (op =) visible T) ? insert (op =) T);
   in rev (fold_proof_terms_types (fold_types add_hiddenT) add_hiddenT proof []) end;
 
-fun standard_hidden_types term proof =
+fun standard_hidden_types prop proof =
   let
-    val hidden = hidden_types term proof;
-    val idx = Term.maxidx_term term (maxidx_proof proof ~1) + 1;
+    val hidden = hidden_types prop proof;
+    val idx = Term.maxidx_term prop (maxidx_proof proof ~1) + 1;
     fun smash T =
       if member (op =) hidden T then
         (case Type.sort_of_atyp T of
@@ -2096,11 +2093,11 @@
     val smashT = map_atyps smash;
   in map_proof_terms (map_types smashT) smashT proof end;
 
-fun standard_hidden_terms term proof =
+fun standard_hidden_terms prop proof =
   let
     fun add_unless excluded x =
       ((is_Free x orelse is_Var x) andalso not (member (op =) excluded x)) ? insert (op =) x;
-    val visible = fold_aterms (add_unless []) term [];
+    val visible = fold_aterms (add_unless []) prop [];
     val hidden = fold_proof_terms (fold_aterms (add_unless visible)) proof [];
     val dummy_term = Term.map_aterms (fn x =>
       if member (op =) hidden x then Term.dummy_pattern (Term.fastype_of x) else x);
@@ -2113,12 +2110,12 @@
     val proofs = opt_proof
       |> Option.map (standard_hidden_types term #> standard_hidden_terms term) |> the_list;
     val proof_terms = rev (fold (fold_proof_terms_types cons (cons o Logic.mk_type)) proofs []);
-    val used_frees = used
+    val used' = used
       |> used_frees_term term
       |> fold used_frees_proof proofs;
-    val inst = Term_Subst.zero_var_indexes_inst used_frees (term :: proof_terms);
-    val term' = term |> Term_Subst.instantiate inst |> unvarify |> variant_term [];
-    val proofs' = proofs |> map (instantiate inst #> unvarify_proof #> variant_proof []);
+    val inst = Term_Subst.zero_var_indexes_inst used' (term :: proof_terms);
+    val term' = term |> Term_Subst.instantiate inst |> unvarify_term |> variant_term Name.context;
+    val proofs' = proofs |> map (instantiate inst #> unvarify_proof #> variant_proof Name.context);
   in (term', try hd proofs') end;
 
 fun standard_vars_term used t = #1 (standard_vars used (t, NONE));
diff -r 1effd04264cc -r 9efbbad0a834 src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Sat Jul 20 16:47:04 2024 +0100
+++ b/src/Pure/term_subst.ML	Sat Jul 20 22:43:27 2024 +0200
@@ -230,7 +230,7 @@
 (* zero var indexes *)
 
 fun zero_var_inst ins mk (v as ((x, i), X)) (inst, used) =
-  let val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used
+  let val (x', used') = Name.variant_bound x used
   in if x = x' andalso i = 0 then (inst, used') else (ins (v, mk ((x', 0), X)) inst, used') end;
 
 fun zero_var_indexes_inst used ts =
diff -r 1effd04264cc -r 9efbbad0a834 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Sat Jul 20 16:47:04 2024 +0100
+++ b/src/Pure/zterm.ML	Sat Jul 20 22:43:27 2024 +0200
@@ -52,6 +52,50 @@
   | fold_types _ _ = I;
 
 
+(* map *)
+
+fun map_tvars_same f =
+  let
+    fun typ (ZTVar v) = f v
+      | typ (ZFun (T, U)) =
+          (ZFun (typ T, Same.commit typ U)
+            handle Same.SAME => ZFun (T, typ U))
+      | typ ZProp = raise Same.SAME
+      | typ (ZType0 _) = raise Same.SAME
+      | typ (ZType1 (a, T)) = ZType1 (a, typ T)
+      | typ (ZType (a, Ts)) = ZType (a, Same.map typ Ts);
+  in typ end;
+
+fun map_aterms_same f =
+  let
+    fun term (ZAbs (x, T, t)) = ZAbs (x, T, term t)
+      | term (ZApp (t, u)) =
+          (ZApp (term t, Same.commit term u)
+            handle Same.SAME => ZApp (t, term u))
+      | term a = f a;
+  in term end;
+
+fun map_types_same f =
+  let
+    fun term (ZVar (xi, T)) = ZVar (xi, f T)
+      | term (ZBound _) = raise Same.SAME
+      | term (ZConst0 _) = raise Same.SAME
+      | term (ZConst1 (c, T)) = ZConst1 (c, f T)
+      | term (ZConst (c, Ts)) = ZConst (c, Same.map f Ts)
+      | term (ZAbs (x, T, t)) =
+          (ZAbs (x, f T, Same.commit term t)
+            handle Same.SAME => ZAbs (x, T, term t))
+      | term (ZApp (t, u)) =
+          (ZApp (term t, Same.commit term u)
+            handle Same.SAME => ZApp (t, term u))
+      | term (OFCLASS (T, c)) = OFCLASS (f T, c);
+  in term end;
+
+val map_tvars = Same.commit o map_tvars_same;
+val map_aterms = Same.commit o map_aterms_same;
+val map_types = Same.commit o map_types_same;
+
+
 (* type ordering *)
 
 local
@@ -224,6 +268,9 @@
   val fold_aterms: (zterm -> 'a -> 'a) -> zterm -> 'a -> 'a
   val fold_vars: (indexname * ztyp -> 'a -> 'a) -> zterm -> 'a -> 'a
   val fold_types: (ztyp -> 'a -> 'a) -> zterm -> 'a -> 'a
+  val map_tvars: (indexname * sort -> ztyp) -> ztyp -> ztyp
+  val map_aterms: (zterm -> zterm) -> zterm -> zterm
+  val map_types: (ztyp -> ztyp) -> zterm -> zterm
   val ztyp_ord: ztyp ord
   val fast_zterm_ord: zterm ord
   val aconv_zterm: zterm * zterm -> bool
@@ -247,6 +294,8 @@
   val subst_term_same:
     ztyp Same.operation -> (indexname * ztyp, zterm) Same.function -> zterm Same.operation
   exception BAD_INST of ((indexname * ztyp) * zterm) list
+  val fold_proof: {hyps: bool} -> (ztyp -> 'a -> 'a) -> (zterm -> 'a -> 'a) -> zproof -> 'a -> 'a
+  val fold_proof_types: {hyps: bool} -> (ztyp -> 'a -> 'a) -> zproof -> 'a -> 'a
   val map_proof: {hyps: bool} -> ztyp Same.operation -> zterm Same.operation -> zproof -> zproof
   val map_proof_types: {hyps: bool} -> ztyp Same.operation -> zproof -> zproof
   val map_class_proof: (ztyp * class, zproof) Same.function -> zproof -> zproof