diff -r 363b557c17a4 -r da932f511746 src/HOL/String.thy
--- 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"