--- a/src/HOL/Imperative_HOL/Heap.thy Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap.thy Tue May 19 16:54:55 2009 +0200
@@ -28,11 +28,11 @@
instance int :: heap ..
-instance message_string :: countable
- by (rule countable_classI [of "message_string_case to_nat"])
- (auto split: message_string.splits)
+instance String.literal :: countable
+ by (rule countable_classI [of "String.literal_case to_nat"])
+ (auto split: String.literal.splits)
-instance message_string :: heap ..
+instance String.literal :: heap ..
text {* Reflected types themselves are heap-representable *}