src/HOL/Code_Generator.thy

--- a/src/HOL/Code_Generator.thy	Thu Mar 22 13:36:57 2007 +0100
+++ b/src/HOL/Code_Generator.thy	Thu Mar 22 14:03:30 2007 +0100
@@ -175,8 +175,8 @@
 text {* code generation for undefined as exception *}
 
 code_const undefined
-  (SML "(raise Fail \"undefined\")")
-  (OCaml "(failwith \"undefined\")")
+  (SML "raise/ Fail/ \"undefined\"")
+  (OCaml "failwith/ \"undefined\"")
   (Haskell "error/ \"undefined\"")
 
 code_reserved SML Fail