# HG changeset patch
# User haftmann
# Date 1179424161 -7200
# Node ID 5f82c5f8478e94c0b5036eed89b21ef74cf7e858
# Parent  d8b4f2dc2b1da6ecd9c9fb729025a34097d01def
dropped beta/eta normalization of defining equations

diff -r d8b4f2dc2b1d -r 5f82c5f8478e src/Pure/Tools/codegen_func.ML
--- 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