# HG changeset patch
# User wenzelm
# Date 1701940011 -3600
# Node ID 23a611444c99dee17546df93231d7033e3c48c92
# Parent  9ddcaca41ed2a1353b115f40e50a25fbae10f0ea
clarified signature;

diff -r 9ddcaca41ed2 -r 23a611444c99 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Dec 07 09:58:12 2023 +0100
+++ b/src/Pure/proofterm.ML	Thu Dec 07 10:06:51 2023 +0100
@@ -110,7 +110,7 @@
   val prf_loose_Pbvar1: proof -> int -> bool
   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': 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 freeze_thaw_prf: proof -> proof * (proof -> proof)
@@ -784,7 +784,7 @@
 fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) =
   Envir.Envir {maxidx = maxidx, tenv = Vartab.map (K (apsnd remove_types)) tenv, tyenv = tyenv};
 
-fun norm_proof' env prf = norm_proof (remove_types_env env) prf;
+fun norm_proof_remove_types env prf = norm_proof (remove_types_env env) prf;
 
 
 (* substitution of bound variables *)
diff -r 9ddcaca41ed2 -r 23a611444c99 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Dec 07 09:58:12 2023 +0100
+++ b/src/Pure/thm.ML	Thu Dec 07 10:06:51 2023 +0100
@@ -1660,7 +1660,7 @@
               val tpairs' = tpairs |> map (apply2 (Envir.norm_term env))
                 (*remove trivial tpairs, of the form t \<equiv> t*)
                 |> filter_out (op aconv);
-              val der' = deriv_rule1 (Proofterm.norm_proof' env, ZTerm.todo_proof) der;
+              val der' = deriv_rule1 (Proofterm.norm_proof_remove_types env, ZTerm.todo_proof) der;
               val thy' = Context.certificate_theory cert' handle ERROR msg =>
                 raise CONTEXT (msg, [], [], [th], Option.map Context.Proof opt_ctxt);
               val constraints' = insert_constraints_env thy' env constraints;
@@ -2050,7 +2050,7 @@
           raise CONTEXT (msg, [], [], [state], Option.map Context.Proof opt_ctxt);
       in
         Thm (deriv_rule1
-          (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof' env,
+          (assumption_proof #> not (Envir.is_empty env) ? Proofterm.norm_proof_remove_types env,
             ZTerm.todo_proof) der,
          {tags = [],
           maxidx = Envir.maxidx_of env,
@@ -2313,8 +2313,9 @@
            val th =
              Thm (deriv_rule2
                    (if Envir.is_empty env then bicompose_proof
-                    else if Envir.above env smax then bicompose_proof o Proofterm.norm_proof' env
-                    else Proofterm.norm_proof' env oo bicompose_proof,
+                    else if Envir.above env smax
+                    then bicompose_proof o Proofterm.norm_proof_remove_types env
+                    else Proofterm.norm_proof_remove_types env oo bicompose_proof,
                     K ZTerm.todo_proof) rder' sder,
                 {tags = [],
                  maxidx = Envir.maxidx_of env,