
diff -r de15ea8fb348 -r b20bc8029edb src/HOL/Code_Generator.thy
--- 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




