more operations;

--- a/src/Pure/zterm.ML	Mon Dec 18 22:49:33 2023 +0100
+++ b/src/Pure/zterm.ML	Tue Dec 19 12:30:46 2023 +0100
@@ -250,6 +250,10 @@
   val zterm_of: theory -> term -> zterm
   val typ_of: ztyp -> typ
   val term_of: theory -> zterm -> term
+  val beta_norm_term_same: zterm Same.operation
+  val beta_norm_proof_same: zproof Same.operation
+  val beta_norm_term: zterm -> zterm
+  val beta_norm_proof: zproof -> zproof
   val norm_type: Type.tyenv -> ztyp -> ztyp
   val norm_term: theory -> Envir.env -> zterm -> zterm
   val norm_proof: theory -> Envir.env -> term list -> zproof -> zproof
@@ -573,7 +577,7 @@
   in term end;
 
 
-(* beta normalization wrt. environment *)
+(* beta contraction *)
 
 val beta_norm_term_same =
   let
@@ -606,6 +610,12 @@
       | norm _ = raise Same.SAME;
   in norm end;
 
+val beta_norm_term = Same.commit beta_norm_term_same;
+val beta_norm_proof = Same.commit beta_norm_proof_same;
+
+
+(* normalization wrt. environment and beta contraction *)
+
 fun norm_type_same ztyp tyenv =
   if Vartab.is_empty tyenv then Same.same
   else