# 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