--- a/src/Pure/Tools/codegen_data.ML Fri Jan 05 14:31:48 2007 +0100
+++ b/src/Pure/Tools/codegen_data.ML Fri Jan 05 14:31:49 2007 +0100
@@ -2,8 +2,8 @@
ID: $Id$
Author: Florian Haftmann, TU Muenchen
-Abstract executable content of theory. Management of data dependent on
-executabl content.
+Abstract executable content of theory. Management of data dependent on
+executable content.
*)
signature CODEGEN_DATA =
@@ -240,6 +240,7 @@
|> try (map snd o mk_func thy)
|> these
|> map (constrain thm)
+ |> map (CodegenFunc.expand_eta thy ~1)
| NONE => []
end;