src/Pure/Tools/codegen_package.ML

     (merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2));
   fun print _ _ = ();
 end);
 
 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 =

       |> ensure_def_class thy algbr funcgr strct ((the o AxClass.class_of_param thy) c)
       |-> (fn _ => succeed CodegenThingol.Bot);
     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;
               fun exprgen_eq (args, rhs) trns =
                 trns