# HG changeset patch
# User berghofe
# Date 1191853709 -7200
# Node ID 49f002c3964ea628add4474cda8c6584dcdc06b5
# Parent  d3cbf79769b9b92ec5f5d021c48e92fed3b51eab
list_codegen and char_codegen now call invoke_tycodegen to ensure
that gen_... and term_of_... functions are generated as well.

diff -r d3cbf79769b9 -r 49f002c3964e src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Oct 08 08:04:28 2007 +0200
+++ b/src/HOL/List.thy	Mon Oct 08 16:28:29 2007 +0200
@@ -3077,14 +3077,21 @@
 let
 
 fun list_codegen thy defs gr dep thyname b t =
-  let val (gr', ps) = foldl_map (Codegen.invoke_codegen thy defs dep thyname false)
-    (gr, HOLogic.dest_list t)
-  in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
+  let
+    val ts = HOLogic.dest_list t;
+    val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false
+      (gr, fastype_of t);
+    val (gr'', ps) = foldl_map
+      (Codegen.invoke_codegen thy defs dep thyname false) (gr', ts)
+  in SOME (gr'', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
 
 fun char_codegen thy defs gr dep thyname b t =
-  case Option.map chr (try HOLogic.dest_char t) of
-      SOME c => SOME (gr, Pretty.quote (Pretty.str (ML_Syntax.print_char c)))
-    | NONE => NONE;
+  let
+    val i = HOLogic.dest_char t;
+    val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false
+      (gr, fastype_of t)
+  in SOME (gr', Pretty.str (ML_Syntax.print_string (chr i)))
+  end handle TERM _ => NONE;
 
 in
   Codegen.add_codegen "list_codegen" list_codegen