# HG changeset patch
# User wenzelm
# Date 1702207102 -3600
# Node ID b79030f610cad0b83ee95ab18aa1b41c3997c46f
# Parent  e81b7689b26404af4837f67223db74bde1c39917
clarified modules;

diff -r e81b7689b264 -r b79030f610ca src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Dec 10 11:56:56 2023 +0100
+++ b/src/Pure/proofterm.ML	Sun Dec 10 12:18:22 2023 +0100
@@ -613,14 +613,6 @@
   | change_types _ prf = prf;
 
 
-(* utilities *)
-
-fun strip_abs (_::Ts) (Abs (_, _, t)) = strip_abs Ts t
-  | strip_abs _ t = t;
-
-fun mk_abs Ts t = Library.foldl (fn (t', T) => Abs ("", T, t')) (t, Ts);
-
-
 (*Abstraction of a proof term over its occurrences of v,
     which must contain no loose bound variables.
   The resulting proof term is ready to become the body of an Abst.*)
@@ -1021,7 +1013,9 @@
     val typs = Same.map_option (Same.map typ);
 
     fun term Us Ts t =
-      strip_abs Ts (Logic.incr_indexes_same ([], Us, inc) (mk_abs Ts t));
+      fold (fn T => fn u => Abs ("", T, u)) Ts t
+      |> Logic.incr_indexes_same ([], Us, inc)
+      |> Term.strip_abs_body' (length Ts);
 
     fun proof Us Ts (Abst (a, T, p)) =
           (Abst (a, Same.map_option typ T, Same.commit (proof Us (dummyT :: Ts)) p)
diff -r e81b7689b264 -r b79030f610ca src/Pure/term.ML
--- a/src/Pure/term.ML	Sun Dec 10 11:56:56 2023 +0100
+++ b/src/Pure/term.ML	Sun Dec 10 12:18:22 2023 +0100
@@ -127,6 +127,7 @@
   val a_itselfT: typ
   val argument_type_of: term -> int -> typ
   val abs: string * typ -> term -> term
+  val strip_abs_body': int -> term -> term
   val args_of: term -> term list
   val add_tvar_namesT: typ -> indexname list -> indexname list
   val add_tvar_names: term -> indexname list -> indexname list
@@ -401,6 +402,10 @@
 fun strip_abs_vars (Abs (a, T, t)) = strip_abs_vars t |> cons (a, T)
   | strip_abs_vars _ = [];
 
+fun strip_abs_body' 0 t = t
+  | strip_abs_body' n (Abs (_, _, t)) = strip_abs_body' (n - 1) t
+  | strip_abs_body' _ t = t;
+
 
 fun strip_qnt_body qnt =
   let