diff -r 64559e1ca05b -r 1f9f973eed2a src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Apr 24 14:17:58 2018 +0000
@@ -230,8 +230,10 @@
   obtains "r = x" "h' = h"
   using assms by (rule effectE) (simp add: execute_simps)
 
-definition raise :: "string \<Rightarrow> 'a Heap" where \<comment> \<open>the string is just decoration\<close>
-  [code del]: "raise s = Heap (\<lambda>_. None)"
+definition raise :: "String.literal \<Rightarrow> 'a Heap" \<comment> \<open>the literal is just decoration\<close>
+  where "raise s = Heap (\<lambda>_. None)"
+
+code_datatype raise \<comment> \<open>avoid @{const "Heap"} formally\<close>
 
 lemma execute_raise [execute_simps]:
   "execute (raise s) = (\<lambda>_. None)"
@@ -309,7 +311,7 @@
 subsubsection \<open>Assertions\<close>
 
 definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where
-  "assert P x = (if P x then return x else raise ''assert'')"
+  "assert P x = (if P x then return x else raise STR ''assert'')"
 
 lemma execute_assert [execute_simps]:
   "P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
@@ -516,32 +518,17 @@
 
 subsection \<open>Code generator setup\<close>
 
-subsubsection \<open>Logical intermediate layer\<close>
-
-definition raise' :: "String.literal \<Rightarrow> 'a Heap" where
-  [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 *)
-  "raise s = raise' (STR s)"
-  unfolding raise'_def by (simp add: STR_inverse)
-
-code_datatype raise' \<comment> \<open>avoid @{const "Heap"} formally\<close>
-
-
 subsubsection \<open>SML and OCaml\<close>
 
 code_printing type_constructor Heap \<rightharpoonup> (SML) "(unit/ ->/ _)"
 code_printing constant bind \<rightharpoonup> (SML) "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())"
 code_printing constant return \<rightharpoonup> (SML) "!(fn/ ()/ =>/ _)"
-code_printing constant Heap_Monad.raise' \<rightharpoonup> (SML) "!(raise/ Fail/ _)"
+code_printing constant Heap_Monad.raise \<rightharpoonup> (SML) "!(raise/ Fail/ _)"
 
 code_printing type_constructor Heap \<rightharpoonup> (OCaml) "(unit/ ->/ _)"
 code_printing constant bind \<rightharpoonup> (OCaml) "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())"
 code_printing constant return \<rightharpoonup> (OCaml) "!(fun/ ()/ ->/ _)"
-code_printing constant Heap_Monad.raise' \<rightharpoonup> (OCaml) "failwith"
+code_printing constant Heap_Monad.raise \<rightharpoonup> (OCaml) "failwith"
 
 
 subsubsection \<open>Haskell\<close>
@@ -588,7 +575,7 @@
 code_printing type_constructor Heap \<rightharpoonup> (Haskell) "Heap.ST/ Heap.RealWorld/ _"
 code_monad bind Haskell
 code_printing constant return \<rightharpoonup> (Haskell) "return"
-code_printing constant Heap_Monad.raise' \<rightharpoonup> (Haskell) "error"
+code_printing constant Heap_Monad.raise \<rightharpoonup> (Haskell) "error"
 
 
 subsubsection \<open>Scala\<close>
@@ -633,7 +620,7 @@
 code_printing type_constructor Heap \<rightharpoonup> (Scala) "(Unit/ =>/ _)"
 code_printing constant bind \<rightharpoonup> (Scala) "Heap.bind"
 code_printing constant return \<rightharpoonup> (Scala) "('_: Unit)/ =>/ _"
-code_printing constant Heap_Monad.raise' \<rightharpoonup> (Scala) "!sys.error((_))"
+code_printing constant Heap_Monad.raise \<rightharpoonup> (Scala) "!sys.error((_))"
 
 
 subsubsection \<open>Target variants with less units\<close>
@@ -703,7 +690,7 @@
 
 \<close>
 
-hide_const (open) Heap heap guard raise' fold_map
+hide_const (open) Heap heap guard fold_map
 
 end