# HG changeset patch
# User wenzelm
# Date 1702058446 -3600
# Node ID 0d8f0201485c57ce78b2d837ffdd80aa959762e0
# Parent  601aa36071ba70c80e7c148ae1cbf1fa1c3b9041
minor performance tuning: more careful treatment of empty environment;

diff -r 601aa36071ba -r 0d8f0201485c src/Pure/envir.ML
--- a/src/Pure/envir.ML	Fri Dec 08 18:51:18 2023 +0100
+++ b/src/Pure/envir.ML	Fri Dec 08 19:00:46 2023 +0100
@@ -216,14 +216,13 @@
 
 fun norm_type tyenv = Same.commit (norm_type_same tyenv);
 
-fun norm_term_same (envir as Envir {tenv, tyenv, ...}) =
-  if Vartab.is_empty tyenv then norm_term1 tenv
-  else norm_term2 envir;
+fun norm_term_same (envir as Envir {tenv, tyenv, ...}) t =
+  if is_empty envir andalso not (Term.could_beta_contract t) then raise Same.SAME
+  else if Vartab.is_empty tyenv then norm_term1 tenv t else norm_term2 envir t;
 
 fun norm_term envir = Same.commit (norm_term_same envir);
 
-fun beta_norm t =
-  if Term.could_beta_contract t then norm_term init t else t;
+val beta_norm = norm_term init;
 
 end;