src/HOL/Imperative_HOL/Heap_Monad.thy

 subsection {* Code generator setup *}
 
 subsubsection {* Logical intermediate layer *}
 
 definition raise' :: "String.literal \<Rightarrow> 'a Heap" where
-  [code del]: "raise' s = raise (explode s)"
+  [code del]: "raise' s = raise (String.explode s)"
 
 lemma [code_abbrev]: "raise' (STR s) = raise s"
   unfolding raise'_def by (simp add: STR_inverse)
 
 lemma raise_raise': (* FIXME delete candidate *)