# HG changeset patch
# User haftmann
# Date 1275381053 -7200
# Node ID 9d9205e31767a857ad087f10a6b8c1e522c72376
# Parent  ffd587207d5d6211d2d38ee4eed2d7e9a0e347a8
tuned code setup

diff -r ffd587207d5d -r 9d9205e31767 src/HOL/Library/Char_nat.thy
--- a/src/HOL/Library/Char_nat.thy	Mon May 31 22:08:40 2010 +0200
+++ b/src/HOL/Library/Char_nat.thy	Tue Jun 01 10:30:53 2010 +0200
@@ -75,7 +75,7 @@
   unfolding nibble_of_nat_def by auto
 
 lemmas nibble_of_nat_code [code] = nibble_of_nat_simps
-  [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc]
+  [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_Bit0 neg_number_of_Bit1 if_False add_0 add_Suc One_nat_def]
 
 lemma nibble_of_nat_of_nibble: "nibble_of_nat (nat_of_nibble n) = n"
   by (cases n) (simp_all only: nat_of_nibble.simps nibble_of_nat_simps)
@@ -193,12 +193,12 @@
 text {* Code generator setup *}
 
 code_modulename SML
-  Char_nat List
+  Char_nat String
 
 code_modulename OCaml
-  Char_nat List
+  Char_nat String
 
 code_modulename Haskell
-  Char_nat List
+  Char_nat String
 
 end
\ No newline at end of file