--- a/src/HOL/String.thy Wed Oct 09 13:40:14 2013 +0200
+++ b/src/HOL/String.thy Wed Oct 09 15:33:20 2013 +0200
@@ -425,8 +425,13 @@
definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
where [simp, code del]: "abort _ f = f ()"
+lemma abort_cong: "msg = msg' ==> Code.abort msg f = Code.abort msg' f"
+by simp
+
setup {* Sign.map_naming Name_Space.parent_path *}
+setup {* Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong}) *}
+
code_printing constant Code.abort \<rightharpoonup>
(SML) "!(raise/ Fail/ _)"
and (OCaml) "failwith"