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.
dropped beta/eta normalization of defining equations
authorhaftmann
Thu, 17 May 2007 19:49:21 +0200
changeset 22996 5f82c5f8478e
parent 22995 d8b4f2dc2b1d
child 22997 d4f3b015b50b
dropped beta/eta normalization of defining equations
src/Pure/Tools/codegen_func.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Tools/codegen_func.ML	Thu May 17 19:49:20 2007 +0200
+++ b/src/Pure/Tools/codegen_func.ML	Thu May 17 19:49:21 2007 +0200
@@ -109,7 +109,7 @@
     val _ = map (check 0) args;
   in thm end;
 
-val mk_func = assert_func o Conv.fconv_rule Drule.beta_eta_conversion o mk_rew;
+val mk_func = assert_func o (*Conv.fconv_rule Drule.beta_eta_conversion o *)mk_rew;
 
 fun head_func thm =
   let
isabelle