# HG changeset patch
# User haftmann
# Date 1223388434 -7200
# Node ID f29fecd6ddaac7c63946ff90278a675bc2cc694c
# Parent  e79fad5c16a61d6fc771883f00e34df8f4e26a1e
corrected SML undefined

diff -r e79fad5c16a6 -r f29fecd6ddaa src/HOL/Code_Setup.thy
--- a/src/HOL/Code_Setup.thy	Tue Oct 07 11:51:31 2008 +0200
+++ b/src/HOL/Code_Setup.thy	Tue Oct 07 16:07:14 2008 +0200
@@ -49,6 +49,8 @@
 lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
   by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
 
+declare eq [code unfold, code inline del]
+
 declare equals_eq [symmetric, code post]
 
 end
@@ -132,7 +134,7 @@
 text {* undefined *}
 
 code_const undefined
-  (SML "raise/ Fail/ \"undefined\"")
+  (SML "!(raise/ Fail/ \"undefined\")")
   (OCaml "failwith/ \"undefined\"")
   (Haskell "error/ \"undefined\"")