# HG changeset patch
# User berghofe
# Date 1196174689 -3600
# Node ID ca009b7ce693b7600a0c161d349005a46108d97e
# Parent  ba5a2bb7a81ad3bb05b1650eb919e1332e2804ff
Optimized beta_norm: only tries to normalize term when it contains
abstractions.

diff -r ba5a2bb7a81a -r ca009b7ce693 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Tue Nov 27 15:43:31 2007 +0100
+++ b/src/Pure/envir.ML	Tue Nov 27 15:44:49 2007 +0100
@@ -186,7 +186,7 @@
 val norm_term = gen_norm_term false;
 val norm_term_same = gen_norm_term true;
 
-val beta_norm = norm_term (empty 0);
+fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t;
 
 fun norm_type iTs = normTh iTs;
 fun norm_type_same iTs =