src/Pure/envir.ML
changeset 25471 ca009b7ce693
parent 24670 9aae962b1d56
child 26328 b2d6f520172c
     1.1 --- a/src/Pure/envir.ML	Tue Nov 27 15:43:31 2007 +0100
     1.2 +++ b/src/Pure/envir.ML	Tue Nov 27 15:44:49 2007 +0100
     1.3 @@ -186,7 +186,7 @@
     1.4  val norm_term = gen_norm_term false;
     1.5  val norm_term_same = gen_norm_term true;
     1.6  
     1.7 -val beta_norm = norm_term (empty 0);
     1.8 +fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t;
     1.9  
    1.10  fun norm_type iTs = normTh iTs;
    1.11  fun norm_type_same iTs =