# HG changeset patch
# User wenzelm
# Date 1701942409 -3600
# Node ID 4fb0723dc5fc584674fabfdc62fca5e65f1af2f3
# Parent  3f02d4d1937bdfcecec61e87e855c1fcb8c826e8
clarified signature;

diff -r 3f02d4d1937b -r 4fb0723dc5fc src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Thu Dec 07 10:40:59 2023 +0100
+++ b/src/Pure/Proof/extraction.ML	Thu Dec 07 10:46:49 2023 +0100
@@ -567,7 +567,7 @@
           in (
             if T = nullT then AbsP ("R",
               SOME (app_rlz_rews Ts vs (rlz $ nullt $ prop)),
-                Proofterm.prf_subst_bounds [nullt] corr_prf)
+                Proofterm.subst_bounds [nullt] corr_prf)
             else Abst (s, SOME T, AbsP ("R",
               SOME (app_rlz_rews (T :: Ts) vs
                 (rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf)), defs')
diff -r 3f02d4d1937b -r 4fb0723dc5fc src/Pure/Proof/proof_checker.ML
--- a/src/Pure/Proof/proof_checker.ML	Thu Dec 07 10:40:59 2023 +0100
+++ b/src/Pure/Proof/proof_checker.ML	Thu Dec 07 10:46:49 2023 +0100
@@ -37,8 +37,8 @@
   end;
 
 fun pretty_prf thy vs Hs prf =
-  let val prf' = prf |> Proofterm.prf_subst_bounds (map Free vs) |>
-    Proofterm.prf_subst_pbounds (map (Hyp o Thm.prop_of) Hs)
+  let val prf' = prf |> Proofterm.subst_bounds (map Free vs) |>
+    Proofterm.subst_pbounds (map (Hyp o Thm.prop_of) Hs)
   in
     (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
      Syntax.pretty_term_global thy (Proofterm.prop_of prf'))
diff -r 3f02d4d1937b -r 4fb0723dc5fc src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Dec 07 10:40:59 2023 +0100
+++ b/src/Pure/proofterm.ML	Thu Dec 07 10:46:49 2023 +0100
@@ -111,8 +111,8 @@
   val prf_add_loose_bnos: int -> int -> proof -> int list * int list -> int list * int list
   val norm_proof: Envir.env -> proof -> proof
   val norm_proof_remove_types: Envir.env -> proof -> proof
-  val prf_subst_bounds: term list -> proof -> proof
-  val prf_subst_pbounds: proof list -> proof -> proof
+  val subst_bounds: term list -> proof -> proof
+  val subst_pbounds: proof list -> proof -> proof
   val freeze_thaw_prf: proof -> proof * (proof -> proof)
 
   (*proof terms for specific inference rules*)
@@ -789,7 +789,7 @@
 
 (* substitution of bound variables *)
 
-fun prf_subst_bounds args prf =
+fun subst_bounds args prf =
   let
     val n = length args;
     fun subst' lev (Bound i) =
@@ -812,7 +812,7 @@
       | subst _ _ = raise Same.SAME;
   in if null args then prf else Same.commit (subst 0) prf end;
 
-fun prf_subst_pbounds args prf =
+fun subst_pbounds args prf =
   let
     val n = length args;
     fun subst Plev tlev (PBound i) =
@@ -1481,8 +1481,8 @@
 
 fun rewrite_prf tymatch (rules, procs) prf =
   let
-    fun rew _ _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel)
-      | rew _ _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel)
+    fun rew _ _ (Abst (_, _, body) % SOME t) = SOME (subst_bounds [t] body, no_skel)
+      | rew _ _ (AbsP (_, _, body) %% prf) = SOME (subst_pbounds [prf] body, no_skel)
       | rew Ts hs prf =
           (case get_first (fn r => r Ts hs prf) procs of
             NONE => get_first (fn (prf1, prf2) => SOME (prf_subst
@@ -1517,7 +1517,7 @@
     and rew2 Ts hs skel (prf % SOME t) =
           (case prf of
             Abst (_, _, body) =>
-              let val prf' = prf_subst_bounds [t] body
+              let val prf' = subst_bounds [t] body
               in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
           | _ =>
               (case rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf of
@@ -1528,7 +1528,7 @@
       | rew2 Ts hs skel (prf1 %% prf2) =
           (case prf1 of
             AbsP (_, _, body) =>
-              let val prf' = prf_subst_pbounds [prf2] body
+              let val prf' = subst_pbounds [prf2] body
               in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
           | _ =>
             let