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