| changeset 25471 | ca009b7ce693 |
| parent 24670 | 9aae962b1d56 |
| child 26328 | b2d6f520172c |
--- 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 =