| changeset 63616 | ff66974e31be |
| parent 63615 | d786d54efc70 |
| child 63618 | 9c4bb72d1f4f |
--- a/src/Pure/envir.ML Fri Aug 05 20:26:13 2016 +0200 +++ b/src/Pure/envir.ML Fri Aug 05 20:45:58 2016 +0200 @@ -221,7 +221,7 @@ else norm_term2 envir; fun norm_term envir t = norm_term_same envir t handle Same.SAME => t; -fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t; +fun beta_norm t = if Term.has_abs t then norm_term init t else t; end;