added serialization for arbitrary

--- a/src/HOL/HOL.thy	Tue Jan 31 16:15:51 2006 +0100
+++ b/src/HOL/HOL.thy	Tue Jan 31 16:26:18 2006 +0100
@@ -1376,6 +1376,7 @@
   "op *" "IntDef.op_times"
   Not "HOL.not"
   uminus "HOL.uminus"
+  arbitrary "HOL.arbitrary"
 
 code_syntax_tyco bool
   ml (target_atom "bool")
@@ -1397,5 +1398,8 @@
   "op =" (* an intermediate solution *)
     ml (infixl 6 "=")
     haskell (infixl 4 "==")
+  arbitrary
+    ml ("raise/ (Fail/ \"non-defined-result\")")
+    haskell ("error/ \"non-defined result\"")
 
 end