# HG changeset patch
# User wenzelm
# Date 1702845021 -3600
# Node ID b14b289caaf605a29ab27d2fba05dcb858787266
# Parent  90c5aadcc4b262c0f264ce1a16fb13997e4eb325
minor performance tuning: more direct beta_norm;

diff -r 90c5aadcc4b2 -r b14b289caaf6 src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Sun Dec 17 21:12:18 2023 +0100
+++ b/src/Pure/zterm.ML	Sun Dec 17 21:30:21 2023 +0100
@@ -531,6 +531,18 @@
   | could_beta_contract (ZAbs (_, _, b)) = could_beta_contract b
   | could_beta_contract _ = false;
 
+val beta_norm_same =
+  let
+    fun norm (ZApp (ZAbs (_, _, body), t)) = subst_bound t body
+      | norm (ZApp (f, t)) =
+          ((case norm f of
+             ZAbs (_, _, body) => subst_bound t body
+           | nf => ZApp (nf, Same.commit norm t))
+          handle Same.SAME => ZApp (f, norm t))
+      | norm (ZAbs (a, T, t)) = ZAbs (a, T, Same.commit norm t)
+      | norm _ = raise Same.SAME;
+  in norm end;
+
 fun norm_type_same ztyp tyenv =
   if Vartab.is_empty tyenv then Same.same
   else
@@ -575,11 +587,7 @@
            | nf => ZApp (nf, Same.commit norm t))
           handle Same.SAME => ZApp (f, norm t))
       | norm _ = raise Same.SAME;
-  in
-    fn t =>
-      if Envir.is_empty envir andalso not (could_beta_contract t)
-      then raise Same.SAME else norm t
-  end;
+  in fn t => if Envir.is_empty envir then beta_norm_same t else norm t end;
 
 fun norm_proof_cache (cache as {ztyp, ...}) (envir as Envir.Envir {tyenv, ...}) =
   let