--- 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)
--- 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