# HG changeset patch # User haftmann # Date 1153838612 -7200 # Node ID 1be8b181dafa7422be1f3c2604c7b3e1545c069d # Parent 8b22026445af435b1efa0c2035613bd9c035dec9 added code generator serialization for Char diff -r 8b22026445af -r 1be8b181dafa src/HOL/List.thy --- a/src/HOL/List.thy Tue Jul 25 16:43:31 2006 +0200 +++ b/src/HOL/List.thy Tue Jul 25 16:43:32 2006 +0200 @@ -2782,6 +2782,9 @@ ml (target_atom "char") haskell (target_atom "Char") +code_constapp Char + ml (target_atom "(__,/ __)") + setup list_codegen_setup setup CodegenPackage.rename_inconsistent