# HG changeset patch
# User haftmann
# Date 1159196654 -7200
# Node ID cb910529d49d5e78e8fdb938959fa8136d0df14a
# Parent  12952535fc2c9e6b00797ba24194b95d0f370b08
added 'undefined' serializer

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