# HG changeset patch
# User haftmann
# Date 1167915700 -3600
# Node ID d382f901304c935b7d54007fbf4bc8ebb4681635
# Parent  0315ecfd3d5d1cc1becae8fdc63d1be46fca21c5
different handling of eta expansion

diff -r 0315ecfd3d5d -r d382f901304c src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Thu Jan 04 14:01:39 2007 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Thu Jan 04 14:01:40 2007 +0100
@@ -86,6 +86,17 @@
 val _ = Context.add_setup (Code.init #> CodegenPackageData.init);
 
 
+(* preparing function equations *)
+
+fun prep_eqs thy (thms as thm :: _) =
+  let
+    val ty = (Logic.unvarifyT o CodegenData.typ_func thy) thm;
+    val thms' = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
+      then thms
+      else map (CodegenFuncgr.expand_eta thy 1) thms;
+  in (ty, thms') end;
+
+
 (* extraction kernel *)
 
 fun check_strict (false, _) has_seri x =
@@ -268,12 +279,12 @@
     fun defgen_fun trns =
       case CodegenFuncgr.funcs funcgr
         (perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) c_tys)
-       of eq_thms as eq_thm :: _ =>
+       of thms as _ :: _ =>
             let
+              val (ty, eq_thms) = prep_eqs thy thms;
               val timeap = if !timing then Output.timeap_msg ("time for " ^ c')
                 else I;
               val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
-              val ty = (Logic.unvarifyT o CodegenData.typ_func thy) eq_thm;
               val vs = (map dest_TFree o Consts.typargs consts) (c', ty);
               val dest_eqthm =
                 apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify o prop_of;