--- a/src/HOL/Library/EfficientNat.thy Tue Oct 31 09:28:55 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy Tue Oct 31 09:28:56 2006 +0100
@@ -129,12 +129,12 @@
*}
code_const "0::nat"
- (SML target_atom "(0 : IntInf.int)")
- (Haskell target_atom "0")
+ (SML "!(0 : IntInf.int)")
+ (Haskell "0")
code_const "Suc"
- (SML "IntInf.op + (__ + 1)")
- (Haskell "(__ + 1)")
+ (SML "IntInf.+ (__, 1)")
+ (Haskell "!(__ + 1)")
setup {*
CodegenData.del_datatype "nat"
@@ -153,8 +153,8 @@
*}
code_type nat
- (SML target_atom "IntInf.int")
- (Haskell target_atom "Integer")
+ (SML "IntInf.int")
+ (Haskell "Integer")
consts_code
"HOL.zero" :: nat ("0")