corrected SML undefined
authorhaftmann
Tue Oct 07 16:07:14 2008 +0200 (2008-10-07)
changeset 28512f29fecd6ddaa
parent 28511 e79fad5c16a6
child 28513 b0b30fd6c264
corrected SML undefined
src/HOL/Code_Setup.thy
     1.1 --- a/src/HOL/Code_Setup.thy	Tue Oct 07 11:51:31 2008 +0200
     1.2 +++ b/src/HOL/Code_Setup.thy	Tue Oct 07 16:07:14 2008 +0200
     1.3 @@ -49,6 +49,8 @@
     1.4  lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
     1.5    by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
     1.6  
     1.7 +declare eq [code unfold, code inline del]
     1.8 +
     1.9  declare equals_eq [symmetric, code post]
    1.10  
    1.11  end
    1.12 @@ -132,7 +134,7 @@
    1.13  text {* undefined *}
    1.14  
    1.15  code_const undefined
    1.16 -  (SML "raise/ Fail/ \"undefined\"")
    1.17 +  (SML "!(raise/ Fail/ \"undefined\")")
    1.18    (OCaml "failwith/ \"undefined\"")
    1.19    (Haskell "error/ \"undefined\"")
    1.20