src/HOL/HOL.thy

   "op +" "IntDef.op_add"
   "op -" "IntDef.op_minus"
   "op *" "IntDef.op_times"
   Not "HOL.not"
   uminus "HOL.uminus"
+  arbitrary "HOL.arbitrary"
 
 code_syntax_tyco bool
   ml (target_atom "bool")
   haskell (target_atom "Bool")
 

     ml ("if __/ then __/ else __")
     haskell ("if __/ then __/ else __")
   "op =" (* an intermediate solution *)
     ml (infixl 6 "=")
     haskell (infixl 4 "==")
+  arbitrary
+    ml ("raise/ (Fail/ \"non-defined-result\")")
+    haskell ("error/ \"non-defined result\"")
 
 end