Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Optimized beta_norm: only tries to normalize term when it contains
authorberghofe
Tue, 27 Nov 2007 15:44:49 +0100
changeset 25471 ca009b7ce693
parent 25470 ba5a2bb7a81a
child 25472 3276a14d06a6
Optimized beta_norm: only tries to normalize term when it contains abstractions.
src/Pure/envir.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle