# HG changeset patch
# User haftmann
# Date 1214826088 -7200
# Node ID 67330748a72e34645f01c315b1aa136ce3301aec
# Parent  facb528f18343927ae288dcc9e051402cf2cc6f3
code generator setup for "int" also works under eta-contraction

diff -r facb528f1834 -r 67330748a72e src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sat Jun 28 23:52:43 2008 +0200
+++ b/src/HOL/Int.thy	Mon Jun 30 13:41:28 2008 +0200
@@ -1924,7 +1924,7 @@
 lemmas int_aux_code = of_nat_aux_code [where ?'a = int, simplified int_aux_def [symmetric], code]
 
 lemma [code, code unfold, code inline del]:
-  "of_nat n = int_aux n 0"
+  "of_nat = (\<lambda>n. int_aux n 0)"
   by (simp add: int_aux_def of_nat_aux_def)
 
 definition