--- a/src/HOL/Code_Generator.thy Tue Mar 20 10:23:31 2007 +0100
+++ b/src/HOL/Code_Generator.thy Tue Mar 20 15:52:37 2007 +0100
@@ -172,15 +172,12 @@
by rule+
-text {* code generation for arbitrary as exception *}
+text {* code generation for undefined as exception *}
-setup {*
- CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
- #> CodegenSerializer.add_undefined "OCaml" "arbitrary" "(failwith \"arbitrary\")"
-*}
-
-code_const arbitrary
- (Haskell "error/ \"arbitrary\"")
+code_const undefined
+ (SML "(raise Fail \"undefined\")")
+ (OCaml "(failwith \"undefined\")")
+ (Haskell "error/ \"undefined\"")
code_reserved SML Fail
code_reserved OCaml failwith