# HG changeset patch
# User haftmann
# Date 1168003909 -3600
# Node ID e52aef4ab54b14fd4f4b3f704dc47b7a81cd029e
# Parent  0b7aff48622e1996ba82637a2cbc41cd68d282cf
primitive definitions are always eta-expanded

diff -r 0b7aff48622e -r e52aef4ab54b src/Pure/Tools/codegen_data.ML
--- 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;