# HG changeset patch
# User haftmann
# Date 1177587179 -7200
# Node ID ed7d53db217026e3bf5291656fb1893907a84911
# Parent  e3962371f568cab8c4c13ed0f046cacc260a7d32
moved code generation pretty integers and characters to separate theories

diff -r e3962371f568 -r ed7d53db2170 NEWS
--- a/NEWS	Thu Apr 26 13:32:55 2007 +0200
+++ b/NEWS	Thu Apr 26 13:32:59 2007 +0200
@@ -515,6 +515,12 @@
 
 *** HOL ***
 
+* Library/Pretty_Int.thy: maps HOL numerals on target language integer literals
+    when generating code.
+
+* Library/Pretty_Char.thy: maps HOL characters on target language character literals
+    when generating code.
+
 * Library/Commutative_Ring.thy: switched from recdef to function package;
     constants add, mul, pow now curried.  Infix syntax for algebraic operations.
 
diff -r e3962371f568 -r ed7d53db2170 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Apr 26 13:32:55 2007 +0200
+++ b/src/HOL/IsaMakefile	Thu Apr 26 13:32:59 2007 +0200
@@ -204,7 +204,7 @@
   Library/Nested_Environment.thy Library/Zorn.thy\
   Library/Library/ROOT.ML Library/Library/document/root.tex \
   Library/Library/document/root.bib Library/While_Combinator.thy \
-  Library/Product_ord.thy Library/Char_ord.thy \
+  Library/Product_ord.thy Library/Char_nat.thy Library/Char_ord.thy \
   Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \
   Library/Coinductive_List.thy Library/AssocList.thy \
   Library/Parity.thy Library/GCD.thy Library/Binomial.thy \
@@ -212,7 +212,8 @@
   Library/SCT_Definition.thy Library/SCT_Theorem.thy Library/SCT_Interpretation.thy \
   Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \
   Library/SCT_Examples.thy Library/sct.ML \
-  Library/Pure_term.thy Library/Eval.thy
+  Library/Pure_term.thy Library/Eval.thy Library/Pretty_Int.thy \
+  Library/Pretty_Char.thy Library/Pretty_Char_chr.thy
 	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
 
 
diff -r e3962371f568 -r ed7d53db2170 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Thu Apr 26 13:32:55 2007 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Thu Apr 26 13:32:59 2007 +0200
@@ -7,7 +7,7 @@
 header {* Weak normalization for simply-typed lambda calculus *}
 
 theory WeakNorm
-imports Type
+imports Type Pretty_Int
 begin
 
 text {*
diff -r e3962371f568 -r ed7d53db2170 src/HOL/Library/Char_nat.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Char_nat.thy	Thu Apr 26 13:32:59 2007 +0200
@@ -0,0 +1,202 @@
+(*  Title:      HOL/Library/Char_nat.thy
+    ID:         $Id$
+    Author:     Norbert Voelker, Florian Haftmann
+*)
+
+header {* Mapping between characters and natural numbers *}
+
+theory Char_nat
+imports List
+begin
+
+text {* Conversions between nibbles and natural numbers in [0..15]. *}
+
+fun
+  nat_of_nibble :: "nibble \<Rightarrow> nat" where
+  "nat_of_nibble Nibble0 = 0"
+  | "nat_of_nibble Nibble1 = 1"
+  | "nat_of_nibble Nibble2 = 2"
+  | "nat_of_nibble Nibble3 = 3"
+  | "nat_of_nibble Nibble4 = 4"
+  | "nat_of_nibble Nibble5 = 5"
+  | "nat_of_nibble Nibble6 = 6"
+  | "nat_of_nibble Nibble7 = 7"
+  | "nat_of_nibble Nibble8 = 8"
+  | "nat_of_nibble Nibble9 = 9"
+  | "nat_of_nibble NibbleA = 10"
+  | "nat_of_nibble NibbleB = 11"
+  | "nat_of_nibble NibbleC = 12"
+  | "nat_of_nibble NibbleD = 13"
+  | "nat_of_nibble NibbleE = 14"
+  | "nat_of_nibble NibbleF = 15"
+
+definition
+  nibble_of_nat :: "nat \<Rightarrow> nibble" where
+  "nibble_of_nat x = (let y = x mod 16 in
+    if y = 0 then Nibble0 else
+    if y = 1 then Nibble1 else
+    if y = 2 then Nibble2 else
+    if y = 3 then Nibble3 else
+    if y = 4 then Nibble4 else
+    if y = 5 then Nibble5 else
+    if y = 6 then Nibble6 else
+    if y = 7 then Nibble7 else
+    if y = 8 then Nibble8 else
+    if y = 9 then Nibble9 else
+    if y = 10 then NibbleA else
+    if y = 11 then NibbleB else
+    if y = 12 then NibbleC else
+    if y = 13 then NibbleD else
+    if y = 14 then NibbleE else
+    NibbleF)"
+
+lemma nibble_of_nat_norm:
+  "nibble_of_nat (n mod 16) = nibble_of_nat n"
+  unfolding nibble_of_nat_def Let_def by auto
+
+lemmas [code func] = nibble_of_nat_norm [symmetric]
+
+lemma nibble_of_nat_simps [simp]:
+  "nibble_of_nat  0 = Nibble0"
+  "nibble_of_nat  1 = Nibble1"
+  "nibble_of_nat  2 = Nibble2"
+  "nibble_of_nat  3 = Nibble3"
+  "nibble_of_nat  4 = Nibble4"
+  "nibble_of_nat  5 = Nibble5"
+  "nibble_of_nat  6 = Nibble6"
+  "nibble_of_nat  7 = Nibble7"
+  "nibble_of_nat  8 = Nibble8"
+  "nibble_of_nat  9 = Nibble9"
+  "nibble_of_nat 10 = NibbleA"
+  "nibble_of_nat 11 = NibbleB"
+  "nibble_of_nat 12 = NibbleC"
+  "nibble_of_nat 13 = NibbleD"
+  "nibble_of_nat 14 = NibbleE"
+  "nibble_of_nat 15 = NibbleF"
+  unfolding nibble_of_nat_def Let_def by auto
+
+lemmas nibble_of_nat_code [code func] = nibble_of_nat_simps
+  [simplified nat_number Let_def not_neg_number_of_Pls neg_number_of_BIT if_False add_0 add_Suc]
+
+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)
+
+lemma nat_of_nibble_of_nat: "nat_of_nibble (nibble_of_nat n) = n mod 16"
+proof -
+  have nibble_nat_enum: "n mod 16 \<in> {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15}"
+  proof -
+    have set_unfold: "\<And>n. {0..Suc n} = insert (Suc n) {0..n}" by auto
+    have "(n\<Colon>nat) mod 16 \<in> {0..Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc
+      (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))}" by simp
+    from this [simplified set_unfold atLeastAtMost_singleton]
+    show ?thesis by auto
+  qed
+  then show ?thesis unfolding nibble_of_nat_def Let_def
+  by auto
+qed
+
+lemma inj_nat_of_nibble: "inj nat_of_nibble"
+  by (rule inj_on_inverseI) (rule nibble_of_nat_of_nibble)
+
+lemma nat_of_nibble_eq: "nat_of_nibble n = nat_of_nibble m \<longleftrightarrow> n = m"
+  by (rule inj_eq) (rule inj_nat_of_nibble)
+
+lemma nat_of_nibble_less_16: "nat_of_nibble n < 16"
+  by (cases n) auto
+
+lemma nat_of_nibble_div_16: "nat_of_nibble n div 16 = 0"
+  by (cases n) auto
+
+
+text {* Conversion between chars and nats. *}
+
+definition
+  nibble_pair_of_nat :: "nat \<Rightarrow> nibble \<times> nibble"
+where
+  "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat (n mod 16))"
+
+lemma nibble_of_pair [code func]:
+  "nibble_pair_of_nat n = (nibble_of_nat (n div 16), nibble_of_nat n)"
+  unfolding nibble_of_nat_norm [of n, symmetric] nibble_pair_of_nat_def ..
+
+fun
+  nat_of_char :: "char \<Rightarrow> nat" where
+  "nat_of_char (Char n m) = nat_of_nibble n * 16 + nat_of_nibble m"
+
+lemmas [simp del] = nat_of_char.simps
+
+definition
+  char_of_nat :: "nat \<Rightarrow> char" where
+  char_of_nat_def: "char_of_nat n = split Char (nibble_pair_of_nat n)"
+
+lemma Char_char_of_nat:
+  "Char n m = char_of_nat (nat_of_nibble n * 16 + nat_of_nibble m)"
+  unfolding char_of_nat_def Let_def nibble_pair_of_nat_def
+  by (auto simp add: div_add1_eq mod_add1_eq nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
+
+lemma char_of_nat_of_char:
+  "char_of_nat (nat_of_char c) = c"
+  by (cases c) (simp add: nat_of_char.simps, simp add: Char_char_of_nat)
+
+lemma nat_of_char_of_nat:
+  "nat_of_char (char_of_nat n) = n mod 256"
+proof -
+  from mod_div_equality [of n, symmetric, of 16]
+  have mod_mult_self3: "\<And>m k n \<Colon> nat. (k * n + m) mod n = m mod n"
+  proof -
+    fix m k n :: nat
+    show "(k * n + m) mod n = m mod n"
+    by (simp only: mod_mult_self1 [symmetric, of m n k] add_commute)
+  qed
+  from mod_div_decomp [of n 256] obtain k l where n: "n = k * 256 + l"
+    and k: "k = n div 256" and l: "l = n mod 256" by blast
+  have 16: "(0::nat) < 16" by auto
+  have 256: "(256 :: nat) = 16 * 16" by auto
+  have l_256: "l mod 256 = l" using l by auto
+  have l_div_256: "l div 16 * 16 mod 256 = l div 16 * 16"
+    using l by auto
+  have aux2: "(k * 256 mod 16 + l mod 16) div 16 = 0"
+    unfolding 256 mult_assoc [symmetric] mod_mult_self_is_0 by simp
+  have aux3: "(k * 256 + l) div 16 = k * 16 + l div 16"
+    unfolding div_add1_eq [of "k * 256" l 16] aux2 256
+      mult_assoc [symmetric] div_mult_self_is_m [OF 16] by simp
+  have aux4: "(k * 256 + l) mod 16 = l mod 16"
+    unfolding 256 mult_assoc [symmetric] mod_mult_self3 ..
+  show ?thesis
+  by (simp add: nat_of_char.simps char_of_nat_def nibble_of_pair nat_of_nibble_of_nat mod_mult_distrib
+    n aux3 mod_mult_self3 l_256 aux4 mod_add1_eq [of "256 * k"] l_div_256)
+qed
+
+lemma nibble_pair_of_nat_char:
+  "nibble_pair_of_nat (nat_of_char (Char n m)) = (n, m)"
+proof -
+  have nat_of_nibble_256:
+    "\<And>n m. (nat_of_nibble n * 16 + nat_of_nibble m) mod 256 = nat_of_nibble n * 16 + nat_of_nibble m"
+  proof -
+    fix n m
+    have nat_of_nibble_less_eq_15: "\<And>n. nat_of_nibble n \<le> 15"
+    using Suc_leI [OF nat_of_nibble_less_16] by (auto simp add: nat_number)
+    have less_eq_240: "nat_of_nibble n * 16 \<le> 240" using nat_of_nibble_less_eq_15 by auto
+    have "nat_of_nibble n * 16 + nat_of_nibble m \<le> 240 + 15"
+    by (rule add_le_mono [of _ 240 _ 15]) (auto intro: nat_of_nibble_less_eq_15 less_eq_240)
+    then have "nat_of_nibble n * 16 + nat_of_nibble m < 256" (is "?rhs < _") by auto
+    then show "?rhs mod 256 = ?rhs" by auto
+  qed
+  show ?thesis
+  unfolding nibble_pair_of_nat_def Char_char_of_nat nat_of_char_of_nat nat_of_nibble_256
+  by (simp add: add_commute nat_of_nibble_div_16 nibble_of_nat_norm nibble_of_nat_of_nibble)
+qed
+
+
+text {* Code generator setup *}
+
+code_modulename SML
+  Char_nat List
+
+code_modulename OCaml
+  Char_nat List
+
+code_modulename Haskell
+  Char_nat List
+
+end
\ No newline at end of file
diff -r e3962371f568 -r ed7d53db2170 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Thu Apr 26 13:32:55 2007 +0200
+++ b/src/HOL/Library/Library.thy	Thu Apr 26 13:32:59 2007 +0200
@@ -24,6 +24,8 @@
   OptionalSugar
   Parity
   Permutation
+  Pretty_Char_chr
+  Pretty_Int
   Primes
   Quotient
   Ramsey
diff -r e3962371f568 -r ed7d53db2170 src/HOL/Library/MLString.thy
--- a/src/HOL/Library/MLString.thy	Thu Apr 26 13:32:55 2007 +0200
+++ b/src/HOL/Library/MLString.thy	Thu Apr 26 13:32:59 2007 +0200
@@ -18,9 +18,7 @@
   be represented as list of characters which
   is awkward to read. This theory provides a distinguished
   datatype for strings which then by convention
-  are serialized as monolithic ML strings. Note
-  that in Haskell these strings are identified
-  with Haskell strings.
+  are serialized as monolithic ML strings.
 *}
 
 
@@ -28,11 +26,10 @@
 
 datatype ml_string = STR string
 
-fun
-  explode :: "ml_string \<Rightarrow> string"
-where
-  "explode (STR s) = s"
+lemmas [code nofunc] = ml_string.recs ml_string.cases
 
+lemma [code func]: "size (s\<Colon>ml_string) = 0"
+  by (cases s) simp_all
 
 subsection {* ML interface *}
 
@@ -50,34 +47,27 @@
 
 code_type ml_string
   (SML "string")
-  (Haskell "String")
-
-code_const STR
-  (Haskell "_")
 
 setup {*
+let
+  val charr = @{const_name Char}
+  val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
+    @{const_name Nibble2}, @{const_name Nibble3},
+    @{const_name Nibble4}, @{const_name Nibble5},
+    @{const_name Nibble6}, @{const_name Nibble7},
+    @{const_name Nibble8}, @{const_name Nibble9},
+    @{const_name NibbleA}, @{const_name NibbleB},
+    @{const_name NibbleC}, @{const_name NibbleD},
+    @{const_name NibbleE}, @{const_name NibbleF}];
+in
   CodegenSerializer.add_pretty_ml_string "SML"
-    @{const_name Nil} @{const_name Cons} @{const_name STR}
-    ML_Syntax.print_char ML_Syntax.print_string "String.implode"
+    charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR}
+end
 *}
 
-code_const explode
-  (SML "String.explode")
-  (Haskell "_")
-
-code_reserved SML string explode
+code_reserved SML string
 
 code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool"
   (SML "!((_ : string) = _)")
-  (Haskell infixl 4 "==")
-
-code_instance ml_string :: eq (Haskell -)
-
-text {* disable something ugly *}
-
-code_const "ml_string_rec" and "ml_string_case" and "size \<Colon> ml_string \<Rightarrow> nat"
-  (SML "!((_); (_); raise Fail \"ml'_string'_rec\")"
-    and "!((_); (_); raise Fail \"ml'_string'_case\")"
-    and "!((_); raise Fail \"size'_ml'_string\")")
 
 end
diff -r e3962371f568 -r ed7d53db2170 src/HOL/Library/Pretty_Char.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Pretty_Char.thy	Thu Apr 26 13:32:59 2007 +0200
@@ -0,0 +1,50 @@
+(*  Title:      HOL/Library/Pretty_Char.thy
+    ID:         $Id$
+    Author:     Florian Haftmann
+*)
+
+header {* Code generation of pretty characters (and strings) *}
+
+theory Pretty_Char
+imports List
+begin
+
+code_type char
+  (SML "char")
+  (OCaml "char")
+  (Haskell "Char")
+
+setup {*
+let
+  val charr = @{const_name Char}
+  val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
+    @{const_name Nibble2}, @{const_name Nibble3},
+    @{const_name Nibble4}, @{const_name Nibble5},
+    @{const_name Nibble6}, @{const_name Nibble7},
+    @{const_name Nibble8}, @{const_name Nibble9},
+    @{const_name NibbleA}, @{const_name NibbleB},
+    @{const_name NibbleC}, @{const_name NibbleD},
+    @{const_name NibbleE}, @{const_name NibbleF}];
+in
+  fold (fn target => CodegenSerializer.add_pretty_char target charr nibbles)
+    ["SML", "OCaml", "Haskell"]
+  #> CodegenSerializer.add_pretty_list_string "Haskell"
+    @{const_name Nil} @{const_name Cons} charr nibbles
+end
+*}
+
+code_instance char :: eq
+  (Haskell -)
+
+code_reserved SML
+  char
+
+code_reserved OCaml
+  char
+
+code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+  (SML "!((_ : char) = _)")
+  (OCaml "!((_ : char) = _)")
+  (Haskell infixl 4 "==")
+
+end
diff -r e3962371f568 -r ed7d53db2170 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Apr 26 13:32:55 2007 +0200
+++ b/src/HOL/List.thy	Thu Apr 26 13:32:59 2007 +0200
@@ -6,7 +6,7 @@
 header {* The datatype of finite lists *}
 
 theory List
-imports PreList
+imports PreList Recdef
 uses "Tools/string_syntax.ML"
 begin
 
@@ -2653,55 +2653,29 @@
   (OCaml "_ list")
   (Haskell "![_]")
 
+code_reserved SML
+  list
+
+code_reserved OCaml
+  list
+
 code_const Nil
   (SML "[]")
   (OCaml "[]")
   (Haskell "[]")
 
-code_type char
-  (SML "char")
-  (OCaml "char")
-  (Haskell "Char")
-
-code_const Char and char_rec
-    and char_case and "size \<Colon> char \<Rightarrow> nat"
-  (Haskell "error/ \"Char\""
-    and "error/ \"char_rec\"" and "error/ \"char_case\"" and "error/ \"size_char\"")
-
 setup {*
-  fold (uncurry (CodegenSerializer.add_undefined "SML")) [
-      ("List.char.Char", "(raise Fail \"Char\")"),
-      ("List.char.char_rec", "(raise Fail \"char_rec\")"),
-      ("List.char.char_case", "(raise Fail \"char_case\")")
-    ]
-  #> fold (uncurry (CodegenSerializer.add_undefined "OCaml")) [
-      ("List.char.Char", "(failwith \"Char\")"),
-      ("List.char.char_rec", "(failwith \"char_rec\")"),
-      ("List.char.char_case", "(failwith \"char_case\")")
-    ]    
+  fold (fn target => CodegenSerializer.add_pretty_list target
+    @{const_name Nil} @{const_name Cons}
+  ) ["SML", "OCaml", "Haskell"]
 *}
 
-code_const "size \<Colon> char \<Rightarrow> nat"
-  (SML "!(_;/ raise Fail \"size'_char\")")
-  (OCaml "!(_;/ failwith \"size'_char\")")
-
-code_instance list :: eq and char :: eq
-  (Haskell - and -)
+code_instance list :: eq
+  (Haskell -)
 
 code_const "op = \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
-code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
-  (SML "!((_ : char) = _)")
-  (OCaml "!((_ : char) = _)")
-  (Haskell infixl 4 "==")
-
-code_reserved SML
-  list char nil
-
-code_reserved OCaml
-  list char
-
 setup {*
 let
 
@@ -2716,18 +2690,8 @@
     | NONE => NONE;
 
 in
-
   Codegen.add_codegen "list_codegen" list_codegen
   #> Codegen.add_codegen "char_codegen" char_codegen
-  #> CodegenSerializer.add_pretty_list "SML" "List.list.Nil" "List.list.Cons"
-       (Pretty.enum "," "[" "]") NONE (7, "::")
-  #> CodegenSerializer.add_pretty_list "OCaml" "List.list.Nil" "List.list.Cons"
-       (Pretty.enum ";" "[" "]") NONE (6, "::")
-  #> CodegenSerializer.add_pretty_list "Haskell" "List.list.Nil" "List.list.Cons"
-       (Pretty.enum "," "[" "]") (SOME (ML_Syntax.print_char, ML_Syntax.print_string)) (5, ":")
-  #> CodegenPackage.add_appconst
-       ("List.char.Char", CodegenPackage.appgen_char (try HOLogic.dest_char))
-
 end;
 *}
 
@@ -2801,8 +2765,7 @@
   "x mem xs \<longleftrightarrow> x \<in> set xs"
   by (induct xs) auto
 
-lemmas in_set_code [code unfold] =
-  mem_iff [symmetric, THEN eq_reflection]
+lemmas in_set_code [code unfold] = mem_iff [symmetric]
 
 lemma empty_null [code inline]:
   "xs = [] \<longleftrightarrow> null xs"
@@ -2819,8 +2782,7 @@
   "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
   by (induct xs) auto
 
-lemmas list_ball_code [code unfold] =
-  list_all_iff [symmetric, THEN eq_reflection]
+lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
 
 lemma list_all_append [simp]:
   "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
@@ -2839,7 +2801,7 @@
   by (induct xs) simp_all
 
 lemmas list_bex_code [code unfold] =
-  list_ex_iff [symmetric, THEN eq_reflection]
+  list_ex_iff [symmetric]
 
 lemma list_ex_length:
   "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
@@ -2857,60 +2819,51 @@
   "map_filter f P xs = map f (filter P xs)"
   by (induct xs) auto
 
-lemma rev_code [code func, code unfold, code noinline]:
-  "rev xs == itrev xs []"
+lemma rev_code [code func]:
+  "rev xs = itrev xs []"
   by simp
 
+
 text {* code for bounded quantification over nats *}
 
-lemma atMost_upto [code inline]:
+lemma atMost_upto [code unfold]:
   "{..n} = set [0..n]"
   by auto
-lemmas atMost_upto' [code unfold] = atMost_upto [THEN eq_reflection]
-
-lemma atLeast_upt [code inline]:
+
+lemma atLeast_upt [code unfold]:
   "{..<n} = set [0..<n]"
   by auto
-lemmas atLeast_upt' [code unfold] = atLeast_upt [THEN eq_reflection]
-
-lemma greaterThanLessThan_upd [code inline]:
+
+lemma greaterThanLessThan_upd [code unfold]:
   "{n<..<m} = set [Suc n..<m]"
   by auto
-lemmas greaterThanLessThan_upd' [code unfold] = greaterThanLessThan_upd [THEN eq_reflection]
-
-lemma atLeastLessThan_upd [code inline]:
+
+lemma atLeastLessThan_upd [code unfold]:
   "{n..<m} = set [n..<m]"
   by auto
-lemmas atLeastLessThan_upd' [code unfold] = atLeastLessThan_upd [THEN eq_reflection]
-
-lemma greaterThanAtMost_upto [code inline]:
+
+lemma greaterThanAtMost_upto [code unfold]:
   "{n<..m} = set [Suc n..m]"
   by auto
-lemmas greaterThanAtMost_upto' [code unfold] = greaterThanAtMost_upto [THEN eq_reflection]
-
-lemma atLeastAtMost_upto [code inline]:
+
+lemma atLeastAtMost_upto [code unfold]:
   "{n..m} = set [n..m]"
   by auto
-lemmas atLeastAtMost_upto' [code unfold] = atLeastAtMost_upto [THEN eq_reflection]
-
-lemma all_nat_less_eq [code inline]:
+
+lemma all_nat_less_eq [code unfold]:
   "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
   by auto
-lemmas all_nat_less_eq' [code unfold] = all_nat_less_eq [THEN eq_reflection]
-
-lemma ex_nat_less_eq [code inline]:
+
+lemma ex_nat_less_eq [code unfold]:
   "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
   by auto
-lemmas ex_nat_less_eq' [code unfold] = ex_nat_less_eq [THEN eq_reflection]
-
-lemma all_nat_less [code inline]:
+
+lemma all_nat_less [code unfold]:
   "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
   by auto
-lemmas all_nat_less' [code unfold] =  all_nat_less [THEN eq_reflection]
-
-lemma ex_nat_less [code inline]:
+
+lemma ex_nat_less [code unfold]:
   "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
   by auto
-lemmas ex_nat_less' [code unfold] = ex_nat_less [THEN eq_reflection]
-
-end
+
+end
\ No newline at end of file
diff -r e3962371f568 -r ed7d53db2170 src/HOL/ex/Random.thy
--- a/src/HOL/ex/Random.thy	Thu Apr 26 13:32:55 2007 +0200
+++ b/src/HOL/ex/Random.thy	Thu Apr 26 13:32:59 2007 +0200
@@ -5,7 +5,7 @@
 header {* A simple random engine *}
 
 theory Random
-imports State_Monad
+imports State_Monad Pretty_Int
 begin
 
 fun
diff -r e3962371f568 -r ed7d53db2170 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Thu Apr 26 13:32:55 2007 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Thu Apr 26 13:32:59 2007 +0200
@@ -16,8 +16,6 @@
 
   type appgen;
   val add_appconst: string * appgen -> theory -> theory;
-  val appgen_numeral: (term -> IntInf.int option) -> appgen;
-  val appgen_char: (term -> int option) -> appgen;
   val appgen_case: (theory -> term
     -> ((string * typ) list * ((term * typ) * (term * term) list)) option)
     -> appgen;
@@ -432,27 +430,6 @@
 (* parametrized application generators, for instantiation in object logic *)
 (* (axiomatic extensions of extraction kernel *)
 
-fun appgen_numeral int_of_numeral thy algbr funcgr strct (app as (c, ts)) trns =
-  case int_of_numeral (list_comb (Const c, ts))
-   of SOME i =>
-        trns
-        |> pair (CodegenThingol.INum i)
-    | NONE =>
-        trns
-        |> appgen_default thy algbr funcgr strct app;
-
-fun appgen_char char_to_index thy algbr funcgr strct (app as ((_, ty), _)) trns =
-  case (char_to_index o list_comb o apfst Const) app
-   of SOME i =>
-        trns
-        |> exprgen_type thy algbr funcgr strct ty
-        |>> (fn _ => IChar (chr i))
-    | NONE =>
-        trns
-        |> appgen_default thy algbr funcgr strct app;
-
-val debug_term = ref (Bound 0);
-
 fun appgen_case dest_case_expr thy algbr funcgr strct (app as (c_ty, ts)) trns =
   let
     val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
diff -r e3962371f568 -r ed7d53db2170 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Thu Apr 26 13:32:55 2007 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML	Thu Apr 26 13:32:59 2007 +0200
@@ -18,12 +18,15 @@
   val add_syntax_constP: string -> string -> OuterParse.token list
     -> (theory -> theory) * OuterParse.token list;
 
-  val add_pretty_list: string -> string -> string -> (Pretty.T list -> Pretty.T)
-   -> ((string -> string) * (string -> string)) option -> int * string
-   -> theory -> theory;
-  val add_pretty_ml_string: string -> string -> string -> string
-   -> (string -> string) -> (string -> string) -> string -> theory -> theory;
   val add_undefined: string -> string -> string -> theory -> theory;
+  val add_pretty_list: string -> string -> string -> theory -> theory;
+  val add_pretty_list_string: string -> string -> string
+    -> string -> string list -> theory -> theory;
+  val add_pretty_char: string -> string -> string list -> theory -> theory
+  val add_pretty_numeral: string -> string * typ -> string -> string -> string
+    -> string -> string -> theory -> theory;
+  val add_pretty_ml_string: string -> string -> string list -> string
+    -> string -> string -> theory -> theory;
   val add_pretty_imperative_monad_bind: string -> string -> theory -> theory;
 
   type serializer;
@@ -187,7 +190,7 @@
   in (pr_bind' ((v', pat'), ty), vars'') end;
 
 
-(* list, string and monad serializers *)
+(* list, char, string, numeral and monad abstract syntax transformations *)
 
 fun implode_list c_nil c_cons t =
   let
@@ -202,10 +205,42 @@
     | _ => NONE
   end;
 
-fun implode_string mk_char mk_string ts =
-  if forall (fn IChar _ => true | _ => false) ts
-  then (SOME o str o mk_string o implode o map (fn IChar c => mk_char c)) ts
-  else NONE;
+fun decode_char c_nibbles (IConst (c1, _), IConst (c2, _)) =
+      let
+        fun idx c = find_index (curry (op =) c) c_nibbles;
+        fun decode ~1 _ = NONE
+          | decode _ ~1 = NONE
+          | decode n m = SOME (chr (n * 16 + m));
+      in decode (idx c1) (idx c2) end
+  | decode_char _ _ = NONE;
+
+fun implode_string c_char c_nibbles mk_char mk_string ts =
+  let
+    fun implode_char (IConst (c, _) `$ t1 `$ t2) =
+          if c = c_char then decode_char c_nibbles (t1, t2) else NONE
+      | implode_char _ = NONE;
+    val ts' = map implode_char ts;
+  in if forall is_some ts'
+    then (SOME o str o mk_string o implode o map_filter I) ts'
+    else NONE
+  end;
+
+fun implode_numeral c_bit0 c_bit1 c_pls c_min c_bit =
+  let
+    fun dest_bit (IConst (c, _)) = if c = c_bit0 then SOME 0
+          else if c = c_bit1 then SOME 1
+          else NONE
+      | dest_bit _ = NONE;
+    fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0
+          else if c = c_min then SOME ~1
+          else NONE
+      | dest_numeral (IConst (c, _) `$ t1 `$ t2) =
+          if c = c_bit then case (dest_numeral t1, dest_bit t2)
+           of (SOME n, SOME b) => SOME (2 * n + IntInf.fromInt b)
+            | _ => NONE
+          else NONE
+      | dest_numeral _ = NONE;
+  in dest_numeral end;
 
 fun implode_monad c_mbind c_kbind t =
   let
@@ -222,53 +257,6 @@
             | NONE => NONE;
   in CodegenThingol.unfoldr dest_monad t end;
 
-fun pretty_ml_string c_nil c_cons mk_char mk_string target_implode =
-  let
-    fun pretty pr vars fxy [(t, _)] =
-      case implode_list c_nil c_cons t
-       of SOME ts => (case implode_string mk_char mk_string ts
-           of SOME p => p
-            | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr vars BR t])
-        | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr vars BR t]
-  in (1, pretty) end;
-
-fun pretty_list c_nil c_cons mk_list mk_char_string (target_fxy, target_cons) =
-  let
-    fun default pr fxy t1 t2 =
-      brackify_infix (target_fxy, R) fxy [
-        pr (INFX (target_fxy, X)) t1,
-        str target_cons,
-        pr (INFX (target_fxy, R)) t2
-      ];
-    fun pretty pr vars fxy [(t1, _), (t2, _)] =
-      case Option.map (cons t1) (implode_list c_nil c_cons t2)
-       of SOME ts =>
-            (case mk_char_string
-             of SOME (mk_char, mk_string) =>
-                  (case implode_string mk_char mk_string ts
-                   of SOME p => p
-                    | NONE => mk_list (map (pr vars NOBR) ts))
-              | NONE => mk_list (map (pr vars NOBR) ts))
-        | NONE => default (pr vars) fxy t1 t2;
-  in (2, pretty) end;
-
-val pretty_imperative_monad_bind =
-  let
-    fun pretty (pr : CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T)
-          vars fxy [(t1, _), ((v, ty) `|-> t2, _)] =
-            pr vars fxy (ICase ((t1, ty), ([(IVar v, t2)])))
-      | pretty pr vars fxy [(t1, _), (t2, ty2)] =
-          let
-            (*this code suffers from the lack of a proper concept for bindings*)
-            val vs = CodegenThingol.fold_varnames cons t2 [];
-            val v = Name.variant vs "x";
-            val vars' = CodegenNames.intro_vars [v] vars;
-            val var = IVar v;
-            val ty = (hd o fst o CodegenThingol.unfold_fun) ty2;
-          in pr vars' fxy (ICase ((t1, ty), ([(var, t2 `$ var)]))) end;
-  in (2, pretty) end;
-
-
 
 (** name auxiliary **)
 
@@ -372,10 +360,6 @@
               #>> (fn p => concat [str "fn", p, str "=>"]);
             val (ps, vars') = fold_map pr binds vars;
           in brackets (ps @ [pr_term vars' NOBR t']) end
-      | pr_term vars fxy (INum n) =
-          brackets [(str o IntInf.toString) n, str ":", str "IntInf.int"]
-      | pr_term vars _ (IChar c) =
-          (str o prefix "#" o quote o ML_Syntax.print_char) c
       | pr_term vars fxy (t as ICase (_, [_])) =
           let
             val (binds, t') = CodegenThingol.unfold_let t;
@@ -641,19 +625,6 @@
             fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
             val (ps, vars') = fold_map pr binds vars;
           in brackets (str "fun" :: ps @ str "->" @@ pr_term vars' NOBR t') end
-      | pr_term vars fxy (INum n) =
-          if n > IntInf.fromInt 0 then
-            brackify fxy [str "Big_int.big_int_of_int", (str o IntInf.toString) n]
-          else
-            brackify fxy [str "Big_int.big_int_of_int",
-              (str o enclose "(" ")" o prefix "-" o IntInf.toString o op ~) n]
-      | pr_term vars _ (IChar c) =
-          (str o enclose "'" "'")
-            (let val i = ord c
-              in if i < 32 orelse i = 39 orelse i = 92
-                then prefix "\\" (string_of_int i)
-                else c
-              end)
       | pr_term vars fxy (t as ICase (_, [_])) =
           let
             val (binds, t') = CodegenThingol.unfold_let t;
@@ -976,10 +947,9 @@
           |> fold (fold (insert (op =)) o Graph.imm_succs code) names
           |> subtract (op =) names;
         val (modls, _) = (split_list o map dest_name) names;
-        val modl = (the_single o distinct (op =)) modls
+        val modl' = (the_single o distinct (op =) o map name_modl) modls
           handle Empty =>
             error ("Illegal mutual dependencies: " ^ commas (map labelled_name names));
-        val modl' = name_modl modl;
         val modl_explode = NameSpace.explode modl';
         fun add_dep name name'' =
           let
@@ -988,13 +958,14 @@
             map_node modl_explode
               (Graph.add_edge (name, name''))
           else let
-            val (common, (diff1::_, diff2::_)) = chop_prefix (op =) (modl_explode, NameSpace.explode modl'');
+            val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
+              (modl_explode, NameSpace.explode modl'');
           in
             map_node common
               (fn gr => Graph.add_edge_acyclic (diff1, diff2) gr
                 handle Graph.CYCLES _ => error ("Dependency "
-                  ^ quote name
-                  ^ " -> " ^ quote name'' ^ " would result in module dependency cycle"))
+                  ^ quote name ^ " -> " ^ quote name''
+                  ^ " would result in module dependency cycle"))
           end end;
       in
         nsp_nodes
@@ -1155,18 +1126,6 @@
             fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
             val (ps, vars') = fold_map pr binds vars;
           in brackets (str "\\" :: ps @ str "->" @@ pr_term vars' NOBR t') end
-      | pr_term vars fxy (INum n) =
-          if n > IntInf.fromInt 0 then
-            (str o IntInf.toString) n
-          else
-            (str o enclose "(" ")" o Library.prefix "-" o IntInf.toString o IntInf.~) n
-      | pr_term vars fxy (IChar c) =
-          (str o enclose "'" "'")
-            (let val i = (Char.ord o the o Char.fromString) c
-              in if i < 32 orelse i = 39 orelse i = 92
-                then Library.prefix "\\" (string_of_int i)
-                else c
-              end)
       | pr_term vars fxy (t as ICase (_, [_])) =
           let
             val (binds, t) = CodegenThingol.unfold_let t;
@@ -1354,7 +1313,7 @@
   let
     val _ = Option.map File.check destination;
     val empty_names = Name.make_context (reserved_haskell @ reserved_user);
-    val name_modl = mk_modl_name_tab empty_names module_prefix module_alias code
+    val name_modl = mk_modl_name_tab empty_names module_prefix module_alias code;
     fun add_def (name, (def, deps)) =
       let
         val (modl, base) = dest_name name;
@@ -1389,7 +1348,7 @@
             | _ => cons (name, ((NameSpace.append modlname' base', base'), SOME def));
       in
         Symtab.map_default (modlname', ([], ([], (empty_names, empty_names))))
-              (apfst (fold (insert (op =)) deps))
+              (apfst (fold (insert (op = : string * string -> bool)) deps))
         #> `(fn code => add_name ((snd o snd o the o Symtab.lookup code) modlname'))
         #-> (fn (base', names) =>
               (Symtab.map_entry modlname' o apsnd) (fn (defs, _) =>
@@ -1500,10 +1459,10 @@
 (** theory data **)
 
 datatype syntax_expr = SyntaxExpr of {
-  class: ((string * (string -> string option)) * serial) Symtab.table,
+  class: (string * (string -> string option)) Symtab.table,
   inst: unit Symtab.table,
-  tyco: (typ_syntax * serial) Symtab.table,
-  const: (term_syntax * serial) Symtab.table
+  tyco: typ_syntax Symtab.table,
+  const: term_syntax Symtab.table
 };
 
 fun mk_syntax_expr ((class, inst), (tyco, const)) =
@@ -1513,10 +1472,10 @@
 fun merge_syntax_expr (SyntaxExpr { class = class1, inst = inst1, tyco = tyco1, const = const1 },
     SyntaxExpr { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
   mk_syntax_expr (
-    (Symtab.merge (eq_snd (op =)) (class1, class2),
-       Symtab.merge (op =) (inst1, inst2)),
-    (Symtab.merge (eq_snd (op =)) (tyco1, tyco2),
-       Symtab.merge (eq_snd (op =)) (const1, const2))
+    (Symtab.join (K snd) (class1, class2),
+       Symtab.join (K snd) (inst1, inst2)),
+    (Symtab.join (K snd) (tyco1, tyco2),
+       Symtab.join (K snd) (const1, const2))
   );
 
 datatype syntax_modl = SyntaxModl of {
@@ -1585,6 +1544,11 @@
 fun the_syntax_expr (Target { syntax_expr = SyntaxExpr x, ... }) = x;
 fun the_syntax_modl (Target { syntax_modl = SyntaxModl x, ... }) = x;
 
+fun assert_serializer thy target =
+  case Symtab.lookup (CodegenSerializerData.get thy) target
+   of SOME data => target
+    | NONE => error ("Unknown code target language: " ^ quote target);
+
 fun add_serializer (target, seri) thy =
   let
     val _ = case Symtab.lookup (CodegenSerializerData.get thy) target
@@ -1601,9 +1565,7 @@
 
 fun map_seri_data target f thy =
   let
-    val _ = if is_some (Symtab.lookup (CodegenSerializerData.get thy) target)
-      then ()
-      else error ("Unknown code target language: " ^ quote target);
+    val _ = assert_serializer thy target;
   in
     thy
     |> (CodegenSerializerData.map o Symtab.map_entry target o map_target) f
@@ -1631,13 +1593,12 @@
     val reserved = the_reserved data;
     val { alias, prolog } = the_syntax_modl data;
     val { class, inst, tyco, const } = the_syntax_expr data;
-    fun fun_of sys = (Option.map fst oo Symtab.lookup) sys;
     val project = if target = target_diag then I
       else CodegenThingol.project_code
         (Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const) cs;
   in
     project #> seri args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
-      (fun_of class) (fun_of tyco) (fun_of const)
+      (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
   end;
 
 val eval_verbose = ref false;
@@ -1651,7 +1612,6 @@
     val reserved = the_reserved data;
     val { alias, prolog } = the_syntax_modl data;
     val { class, inst, tyco, const } = the_syntax_expr data;
-    fun fun_of sys = (Option.map fst oo Symtab.lookup) sys;
     fun eval p = (
       reff := NONE;
       if !eval_verbose then Pretty.writeln p else ();
@@ -1672,35 +1632,158 @@
           (SOME [val_name])
     |> seri_ml pr_sml pr_sml_modl ML_Syntax.reserved I (labelled_name thy) reserved
         (Symtab.lookup alias) (Symtab.lookup prolog)
-        (fun_of class) (fun_of tyco) (fun_of const)
+        (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
     |> eval
   end;
 
-fun assert_serializer thy target =
-  case Symtab.lookup (CodegenSerializerData.get thy) target
-   of SOME data => target
-    | NONE => error ("Unknown code target language: " ^ quote target);
-
-fun has_serialization f thy targets name =
+fun const_has_serialization thy targets name =
   forall (
-    is_some o (fn tab => Symtab.lookup tab name) o f o the_syntax_expr o the
+    is_some o (fn tab => Symtab.lookup tab name) o #const o the_syntax_expr o the
       o Symtab.lookup (CodegenSerializerData.get thy)
   ) targets;
 
-val const_has_serialization = has_serialization #const;
+
+(** optional pretty serialization **)
+
+local
 
+val pretty : (string * {
+    pretty_char: string -> string,
+    pretty_string: string -> string,
+    pretty_numeral: IntInf.int -> string,
+    pretty_list: Pretty.T list -> Pretty.T,
+    infix_cons: int * string
+  }) list = [
+  ("SML", { pretty_char = prefix "#" o quote o ML_Syntax.print_char,
+      pretty_string = ML_Syntax.print_string,
+      pretty_numeral = fn k => "(" ^ IntInf.toString k ^ " : IntInf.int)",
+      pretty_list = Pretty.enum "," "[" "]",
+      infix_cons = (7, "::")}),
+  ("OCaml", { pretty_char = fn c => enclose "'" "'"
+        (let val i = ord c
+          in if i < 32 orelse i = 39 orelse i = 92
+            then prefix "\\" (string_of_int i)
+            else c
+          end),
+      pretty_string = (fn _ => error "OCaml: no pretty strings"),
+      pretty_numeral = fn k => if k >= IntInf.fromInt 0 then
+            "(Big_int.big_int_of_int " ^ IntInf.toString k ^ ")"
+          else
+            "(Big_int.big_int_of_int " ^ (enclose "(" ")" o prefix "-"
+              o IntInf.toString o op ~) k ^ ")",
+      pretty_list = Pretty.enum ";" "[" "]",
+      infix_cons = (6, "::")}),
+  ("Haskell", { pretty_char = fn c => enclose "'" "'"
+        (let val i = ord c
+          in if i < 32 orelse i = 39 orelse i = 92
+            then Library.prefix "\\" (string_of_int i)
+            else c
+          end),
+      pretty_string = ML_Syntax.print_string,
+      pretty_numeral = fn k => if k >= IntInf.fromInt 0 then
+            IntInf.toString k
+          else
+            (enclose "(" ")" o Library.prefix "-" o IntInf.toString o IntInf.~) k,
+      pretty_list = Pretty.enum "," "[" "]",
+      infix_cons = (5, ":")})
+];
+
+in
+
+fun pr_pretty target = case AList.lookup (op =) pretty target
+ of SOME x => x
+  | NONE => error ("Unknown code target language: " ^ quote target);
+
+fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
+  brackify_infix (target_fxy, R) fxy [
+    pr (INFX (target_fxy, X)) t1,
+    str target_cons,
+    pr (INFX (target_fxy, R)) t2
+  ];
 
+fun pretty_list c_nil c_cons target =
+  let
+    val pretty_ops = pr_pretty target;
+    val mk_list = #pretty_list pretty_ops;
+    fun pretty pr vars fxy [(t1, _), (t2, _)] =
+      case Option.map (cons t1) (implode_list c_nil c_cons t2)
+       of SOME ts => mk_list (map (pr vars NOBR) ts)
+        | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
+  in (2, pretty) end;
 
-(** ML and toplevel interface **)
+fun pretty_list_string c_nil c_cons c_char c_nibbles target =
+  let
+    val pretty_ops = pr_pretty target;
+    val mk_list = #pretty_list pretty_ops;
+    val mk_char = #pretty_char pretty_ops;
+    val mk_string = #pretty_string pretty_ops;
+    fun pretty pr vars fxy [(t1, _), (t2, _)] =
+      case Option.map (cons t1) (implode_list c_nil c_cons t2)
+       of SOME ts => case implode_string c_char c_nibbles mk_char mk_string ts
+           of SOME p => p
+            | NONE => mk_list (map (pr vars NOBR) ts)
+        | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
+  in (2, pretty) end;
+
+fun pretty_char c_char c_nibbles target =
+  let
+    val mk_char = #pretty_char (pr_pretty target);
+    fun pretty _ _ _ [(t1, _), (t2, _)] =
+      case decode_char c_nibbles (t1, t2)
+       of SOME c => (str o mk_char) c
+        | NONE => error "Illegal character expression";
+  in (2, pretty) end;
+
+fun pretty_numeral c_bit0 c_bit1 c_pls c_min c_bit target =
+  let
+    val mk_numeral = #pretty_numeral (pr_pretty target);
+    fun pretty _ _ _ [(t, _)] =
+      case implode_numeral c_bit0 c_bit1 c_pls c_min c_bit t
+       of SOME k => (str o mk_numeral) k
+        | NONE => error "Illegal numeral expression";
+  in (1, pretty) end;
+
+fun pretty_ml_string c_char c_nibbles c_nil c_cons target =
+  let
+    val pretty_ops = pr_pretty target;
+    val mk_char = #pretty_char pretty_ops;
+    val mk_string = #pretty_string pretty_ops;
+    fun pretty pr vars fxy [(t, _)] =
+      case implode_list c_nil c_cons t
+       of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
+           of SOME p => p
+            | NONE => error "Illegal ml_string expression")
+        | NONE => error "Illegal ml_string expression";
+  in (1, pretty) end;
+
+val pretty_imperative_monad_bind =
+  let
+    fun pretty (pr : CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T)
+          vars fxy [(t1, _), ((v, ty) `|-> t2, _)] =
+            pr vars fxy (ICase ((t1, ty), ([(IVar v, t2)])))
+      | pretty pr vars fxy [(t1, _), (t2, ty2)] =
+          let
+            (*this code suffers from the lack of a proper concept for bindings*)
+            val vs = CodegenThingol.fold_varnames cons t2 [];
+            val v = Name.variant vs "x";
+            val vars' = CodegenNames.intro_vars [v] vars;
+            val var = IVar v;
+            val ty = (hd o fst o CodegenThingol.unfold_fun) ty2;
+          in pr vars' fxy (ICase ((t1, ty), ([(var, t2 `$ var)]))) end;
+  in (2, pretty) end;
+
+end; (*local*)
+
+(** ML and Isar interface **)
 
 local
 
 fun map_syntax_exprs target =
-  map_seri_data target o (apsnd o apsnd o apfst o map_syntax_expr);
+  map_seri_data target o apsnd o apsnd o apfst o map_syntax_expr;
 fun map_syntax_modls target =
-  map_seri_data target o (apsnd o apsnd o apsnd o map_syntax_modl);
+  map_seri_data target o apsnd o apsnd o apsnd o map_syntax_modl;
 fun map_reserveds target =
-  map_seri_data target o (apsnd o apfst o apsnd);
+  map_seri_data target o apsnd o apfst o apsnd;
 
 fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
   let
@@ -1716,7 +1799,7 @@
    of SOME (syntax, raw_ops) =>
       thy
       |> (map_syntax_exprs target o apfst o apfst)
-           (Symtab.update (class, ((syntax, mk_syntax_ops raw_ops), serial ())))
+           (Symtab.update (class, (syntax, mk_syntax_ops raw_ops)))
     | NONE =>
       thy
       |> (map_syntax_exprs target o apfst o apfst)
@@ -1747,7 +1830,7 @@
    of SOME syntax =>
       thy
       |> (map_syntax_exprs target o apsnd o apfst)
-           (Symtab.update (tyco', (check_args syntax, serial ())))
+           (Symtab.update (tyco', check_args syntax))
    | NONE =>
       thy
       |> (map_syntax_exprs target o apsnd o apfst)
@@ -1765,7 +1848,7 @@
    of SOME syntax =>
       thy
       |> (map_syntax_exprs target o apsnd o apsnd)
-           (Symtab.update (c', (check_args syntax, serial ())))
+           (Symtab.update (c', check_args syntax))
    | NONE =>
       thy
       |> (map_syntax_exprs target o apsnd o apsnd)
@@ -1881,27 +1964,6 @@
 fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
 fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings);
 
-fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy =
-  let
-    val (_, nil'') = idfs_of_const thy nill;
-    val (cons', cons'') = idfs_of_const thy cons;
-    val pr = pretty_list nil'' cons'' mk_list mk_char_string target_cons;
-  in
-    thy
-    |> add_syntax_const target cons' (SOME pr)
-  end;
-
-fun add_pretty_ml_string target nill cons str mk_char mk_string target_implode thy =
-  let
-    val (_, nil'') = idfs_of_const thy nill;
-    val (_, cons'') = idfs_of_const thy cons;
-    val (str', _) = idfs_of_const thy str;
-    val pr = pretty_ml_string nil'' cons'' mk_char mk_string target_implode;
-  in
-    thy
-    |> add_syntax_const target str' (SOME pr)
-  end;
-
 fun add_undefined target undef target_undefined thy =
   let
     val (undef', _) = idfs_of_const thy undef;
@@ -1911,6 +1973,65 @@
     |> add_syntax_const target undef' (SOME (~1, pr))
   end;
 
+fun add_pretty_list target nill cons thy =
+  let
+    val (_, nil'') = idfs_of_const thy nill;
+    val (cons', cons'') = idfs_of_const thy cons;
+    val pr = pretty_list nil'' cons'' target;
+  in
+    thy
+    |> add_syntax_const target cons' (SOME pr)
+  end;
+
+fun add_pretty_list_string target nill cons charr nibbles thy =
+  let
+    val (_, nil'') = idfs_of_const thy nill;
+    val (cons', cons'') = idfs_of_const thy cons;
+    val (_, charr'') = idfs_of_const thy charr;
+    val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles);
+    val pr = pretty_list_string nil'' cons'' charr'' nibbles'' target;
+  in
+    thy
+    |> add_syntax_const target cons' (SOME pr)
+  end;
+
+fun add_pretty_char target charr nibbles thy =
+  let
+    val (charr', charr'') = idfs_of_const thy charr;
+    val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles);
+    val pr = pretty_char charr'' nibbles'' target;
+  in
+    thy
+    |> add_syntax_const target charr' (SOME pr)
+  end;
+
+fun add_pretty_numeral target number_of b0 b1 pls min bit thy =
+  let
+    val number_of' = CodegenConsts.const_of_cexpr thy number_of;
+    val (_, b0'') = idfs_of_const thy b0;
+    val (_, b1'') = idfs_of_const thy b1;
+    val (_, pls'') = idfs_of_const thy pls;
+    val (_, min'') = idfs_of_const thy min;
+    val (_, bit'') = idfs_of_const thy bit;
+    val pr = pretty_numeral b0'' b1'' pls'' min'' bit'' target;
+  in
+    thy
+    |> add_syntax_const target number_of' (SOME pr)
+  end;
+
+fun add_pretty_ml_string target charr nibbles nill cons str thy =
+  let
+    val (_, charr'') = idfs_of_const thy charr;
+    val (_, nibbles'') = split_list (map (idfs_of_const thy) nibbles);
+    val (_, nil'') = idfs_of_const thy nill;
+    val (_, cons'') = idfs_of_const thy cons;
+    val (str', _) = idfs_of_const thy str;
+    val pr = pretty_ml_string charr'' nibbles'' nil'' cons'' target;
+  in
+    thy
+    |> add_syntax_const target str' (SOME pr)
+  end;
+
 fun add_pretty_imperative_monad_bind target bind thy =
   let
     val (bind', _) = idfs_of_const thy bind;
diff -r e3962371f568 -r ed7d53db2170 src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Thu Apr 26 13:32:55 2007 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Thu Apr 26 13:32:59 2007 +0200
@@ -27,8 +27,6 @@
     | IVar of vname
     | `$ of iterm * iterm
     | `|-> of (vname * itype) * iterm
-    | INum of IntInf.int
-    | IChar of string (*length one!*)
     | ICase of (iterm * itype) * (iterm * iterm) list;
         (*(discriminendum term (td), discriminendum type (ty)),
                 [(selector pattern (p), body term (t))] (bs))*)
@@ -128,8 +126,6 @@
   | IVar of vname
   | `$ of iterm * iterm
   | `|-> of (vname * itype) * iterm
-  | INum of IntInf.int
-  | IChar of string
   | ICase of (iterm * itype) * (iterm * iterm) list;
     (*see also signature*)
 
@@ -198,10 +194,6 @@
       fold_aiterms f t1 #> fold_aiterms f t2
   | fold_aiterms f (t as _ `|-> t') =
       f t #> fold_aiterms f t'
-  | fold_aiterms f (t as INum _) =
-      f t
-  | fold_aiterms f (t as IChar _) =
-      f t
   | fold_aiterms f (ICase ((td, _), bs)) =
       fold_aiterms f td #> fold (fn (p, t) => fold_aiterms f p #> fold_aiterms f t) bs;
 
@@ -228,10 +220,6 @@
           add vs t1 #> add vs t2
       | add vs ((v, _) `|-> t) =
           add (insert (op =) v vs) t
-      | add vs (INum _) =
-          I
-      | add vs (IChar _) =
-          I
       | add vs (ICase ((td, _), bs)) =
           add vs td #> fold (fn (p, t) => add vs p #> add vs t) bs;
   in add [] end;