src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 31205 98370b26c2ce
parent 31058 9f151b096533
child 31724 9b5a128cdb5c
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue May 19 13:57:51 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue May 19 16:54:55 2009 +0200
@@ -274,7 +274,7 @@
 subsubsection {* Logical intermediate layer *}
 
 definition
-  Fail :: "message_string \<Rightarrow> exception"
+  Fail :: "String.literal \<Rightarrow> exception"
 where
   [code del]: "Fail s = Exn"