src/HOL/Imperative_HOL/Heap_Monad.thy

 subsection {* Code generator setup *}
 
 subsubsection {* Logical intermediate layer *}
 
 definition
-  Fail :: "message_string \<Rightarrow> exception"
+  Fail :: "String.literal \<Rightarrow> exception"
 where
   [code del]: "Fail s = Exn"
 
 definition
   raise_exc :: "exception \<Rightarrow> 'a Heap"