# HG changeset patch
# User haftmann
# Date 1166038696 -3600
# Node ID 5a6f8514d0e9e784aa109577af0225aa3397762c
# Parent  1897fe3d72d51d7254b75fed1ab100843dbd2517
clarified character setup

diff -r 1897fe3d72d5 -r 5a6f8514d0e9 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Dec 13 19:39:48 2006 +0100
+++ b/src/HOL/List.thy	Wed Dec 13 20:38:16 2006 +0100
@@ -2555,9 +2555,9 @@
   (SML "char")
   (Haskell "Char")
 
-code_const Char
-  (SML "!((_),/ (_))")
-  (Haskell "!((_),/ (_))")
+code_const Char and char_rec and "size \<Colon> char \<Rightarrow> nat"
+  (SML "raise/ Fail/ \"Char\"" and "raise/ Fail/ \"char_rec\"" and "raise/ Fail/ \"size_char\"")
+  (Haskell "error/ \"Char\"" and "error/ \"char_rec\"" and "error/ \"size_char\"")
 
 code_instance list :: eq and char :: eq
   (Haskell - and -)