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