src/HOL/Library/Code_Message.thy

--- a/src/HOL/Library/Code_Message.thy	Mon Dec 17 18:22:48 2007 +0100
+++ b/src/HOL/Library/Code_Message.thy	Mon Dec 17 18:23:50 2007 +0100
@@ -17,6 +17,9 @@
 lemma [code func]: "size (s\<Colon>message_string) = 0"
   by (cases s) simp_all
 
+lemma [code func]: "message_string_size (s\<Colon>message_string) = 0"
+  by (cases s) simp_all
+
 subsection {* ML interface *}
 
 ML {*