src/HOL/Code_Generator.thy
changeset 22480 b20bc8029edb
parent 22473 753123c89d72
child 22487 8cff8a6cb995
     1.1 --- a/src/HOL/Code_Generator.thy	Tue Mar 20 10:23:31 2007 +0100
     1.2 +++ b/src/HOL/Code_Generator.thy	Tue Mar 20 15:52:37 2007 +0100
     1.3 @@ -172,15 +172,12 @@
     1.4    by rule+
     1.5  
     1.6  
     1.7 -text {* code generation for arbitrary as exception *}
     1.8 +text {* code generation for undefined as exception *}
     1.9  
    1.10 -setup {*
    1.11 -  CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
    1.12 -  #> CodegenSerializer.add_undefined "OCaml" "arbitrary" "(failwith \"arbitrary\")"
    1.13 -*}
    1.14 -
    1.15 -code_const arbitrary
    1.16 -  (Haskell "error/ \"arbitrary\"")
    1.17 +code_const undefined
    1.18 +  (SML "(raise Fail \"undefined\")")
    1.19 +  (OCaml "(failwith \"undefined\")")
    1.20 +  (Haskell "error/ \"undefined\"")
    1.21  
    1.22  code_reserved SML Fail
    1.23  code_reserved OCaml failwith