# HG changeset patch
# User haftmann
# Date 1179567212 -7200
# Node ID db38b8046294b871fe6fcfdc6bda757716772054
# Parent  7507f94adc32cf69b77b7eb267f5e55d020c363c
improved eta expansion

diff -r 7507f94adc32 -r db38b8046294 src/Pure/Tools/codegen_func.ML
--- a/src/Pure/Tools/codegen_func.ML	Sat May 19 11:33:31 2007 +0200
+++ b/src/Pure/Tools/codegen_func.ML	Sat May 19 11:33:32 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 mk_rew;
 
 fun head_func thm =
   let
@@ -161,7 +161,9 @@
     val (vs, _) = get_name rhs l used;
     val vs_refl = map (fn (v, ty) => Thm.reflexive (Thm.cterm_of thy (Var ((v, 0), ty)))) vs;
   in
-    fold (fn refl => fn thm => Thm.combination thm refl) vs_refl thm
+    thm
+    |> fold (fn refl => fn thm => Thm.combination thm refl) vs_refl
+    |> Conv.fconv_rule Drule.beta_eta_conversion
   end;
 
 fun rewrite_func rewrites thm =