src/HOL/Datatype.thy

--- a/src/HOL/Datatype.thy	Tue Mar 07 04:06:02 2006 +0100
+++ b/src/HOL/Datatype.thy	Tue Mar 07 14:09:48 2006 +0100
@@ -246,6 +246,9 @@
   fst_conv [code]
   snd_conv [code]
 
+lemma [code unfold]:
+  "1 == Suc 0" by simp
+
 code_generate True False Not "op &" "op |" If
 
 code_syntax_tyco bool
@@ -311,9 +314,4 @@
     ml (target_atom "SOME")
     haskell (target_atom "Just")
 
-code_syntax_const
-  "1 :: nat"
-    ml ("{*Suc 0*}")
-    haskell ("{*Suc 0*}")
-
 end