src/HOL/Imperative_HOL/Heap.thy
changeset 31205 98370b26c2ce
parent 30738 0842e906300c
child 33639 603320b93668
--- 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 *}