diff -r 12952535fc2c -r cb910529d49d src/HOL/HOL.thy --- a/src/HOL/HOL.thy Mon Sep 25 17:04:12 2006 +0200 +++ b/src/HOL/HOL.thy Mon Sep 25 17:04:14 2006 +0200 @@ -1389,4 +1389,12 @@ in add_itself end; *} +text {* code generation for arbitrary as exception *} + +setup {* + CodegenSerializer.add_undefined "SML" "arbitrary" "raise Fail \"arbitrary\"" +*} +code_const arbitrary + (Haskell target_atom "(error \"arbitrary\")") + end