# HG changeset patch
# User wenzelm
# Date 1702033853 -3600
# Node ID ad98105148e50d742aa787a10d893d8b80de860f
# Parent  90ba93146eb558b1c4acda5702626139f7abc531
clarified signature;

diff -r 90ba93146eb5 -r ad98105148e5 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Fri Dec 08 12:05:56 2023 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Fri Dec 08 12:10:53 2023 +0100
@@ -141,7 +141,7 @@
             (case head_of (strip_abs_body f) of
               Free (s, T) =>
                 let val T' = Logic.varifyT_global T in
-                  Abst (s, SOME T', Proofterm.prf_abstract_over
+                  Abst (s, SOME T', Proofterm.abstract_over
                     (Var ((s, 0), T')) (AbsP ("H", SOME p, prf)))
                 end
             | _ => AbsP ("H", SOME p, prf)))
diff -r 90ba93146eb5 -r ad98105148e5 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Dec 08 12:05:56 2023 +0100
+++ b/src/Pure/proofterm.ML	Fri Dec 08 12:10:53 2023 +0100
@@ -103,7 +103,7 @@
   val maxidx_proof: proof -> int -> int
   val size_of_proof: proof -> int
   val change_types: typ list option -> proof -> proof
-  val prf_abstract_over: term -> proof -> proof
+  val abstract_over: term -> proof -> proof
   val incr_bv_same: int -> int -> int -> int -> proof Same.operation
   val incr_bv: int -> int -> int -> int -> proof -> proof
   val incr_boundvars: int -> int -> proof -> proof
@@ -616,7 +616,7 @@
     which must contain no loose bound variables.
   The resulting proof term is ready to become the body of an Abst.*)
 
-fun prf_abstract_over v =
+fun abstract_over v =
   let
     fun term lev u =
       if v aconv u then Bound lev
@@ -926,7 +926,7 @@
 
 (* forall introduction *)
 
-fun forall_intr_proof (a, v) opt_T prf = Abst (a, opt_T, prf_abstract_over v prf);
+fun forall_intr_proof (a, v) opt_T prf = Abst (a, opt_T, abstract_over v prf);
 
 fun forall_intr_proof' v prf =
   let val (a, T) = (case v of Var ((a, _), T) => (a, T) | Free (a, T) => (a, T))