# HG changeset patch
# User berghofe
# Date 1181927963 -7200
# Node ID 1766da98eaa9a7f0b89d84e31917bd09510e06c0
# Parent  0b5a400c7595e1678ef43f37d5dc61044ae34894
Locally added definition of "int :: nat => int" again to make
code generation work.

diff -r 0b5a400c7595 -r 1766da98eaa9 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Fri Jun 15 15:10:32 2007 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Fri Jun 15 19:19:23 2007 +0200
@@ -575,6 +575,10 @@
   CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
 *}
 
+definition
+  int :: "nat \<Rightarrow> int" where
+  "int \<equiv> of_nat"
+
 code_gen type_NF nat int in SML
 
 ML {*
@@ -584,7 +588,7 @@
 structure Nat = ROOT.Nat;
 
 val nat_of_int = ROOT.Integer.nat o IntInf.fromInt;
-val int_of_nat = IntInf.toInt o ROOT.Integer.int;
+val int_of_nat = IntInf.toInt o ROOT.WeakNorm.int;
 
 fun dBtype_of_typ (Type ("fun", [T, U])) =
       Type.Fun (dBtype_of_typ T, dBtype_of_typ U)