Locally added definition of "int :: nat => int" again to make
authorberghofe
Fri Jun 15 19:19:23 2007 +0200 (2007-06-15)
changeset 233991766da98eaa9
parent 23398 0b5a400c7595
child 23400 a64b39e5809b
Locally added definition of "int :: nat => int" again to make
code generation work.
src/HOL/Lambda/WeakNorm.thy
     1.1 --- a/src/HOL/Lambda/WeakNorm.thy	Fri Jun 15 15:10:32 2007 +0200
     1.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Fri Jun 15 19:19:23 2007 +0200
     1.3 @@ -575,6 +575,10 @@
     1.4    CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
     1.5  *}
     1.6  
     1.7 +definition
     1.8 +  int :: "nat \<Rightarrow> int" where
     1.9 +  "int \<equiv> of_nat"
    1.10 +
    1.11  code_gen type_NF nat int in SML
    1.12  
    1.13  ML {*
    1.14 @@ -584,7 +588,7 @@
    1.15  structure Nat = ROOT.Nat;
    1.16  
    1.17  val nat_of_int = ROOT.Integer.nat o IntInf.fromInt;
    1.18 -val int_of_nat = IntInf.toInt o ROOT.Integer.int;
    1.19 +val int_of_nat = IntInf.toInt o ROOT.WeakNorm.int;
    1.20  
    1.21  fun dBtype_of_typ (Type ("fun", [T, U])) =
    1.22        Type.Fun (dBtype_of_typ T, dBtype_of_typ U)