src/HOL/HOL.thy
changeset 20833 4fcf8ddb54f5
parent 20766 9913d3bc3d17
child 20944 34b2c1bb7178
equal deleted inserted replaced
20832:c3828205f22d 20833:4fcf8ddb54f5
  1386 *} 
  1386 *} 
  1387 
  1387 
  1388 text {* code generation for arbitrary as exception *}
  1388 text {* code generation for arbitrary as exception *}
  1389 
  1389 
  1390 setup {*
  1390 setup {*
  1391   CodegenSerializer.add_undefined "SML" "arbitrary" "raise Fail \"arbitrary\""
  1391   CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
  1392 *}
  1392 *}
  1393 code_const arbitrary
  1393 code_const arbitrary
  1394   (Haskell target_atom "(error \"arbitrary\")")
  1394   (Haskell target_atom "(error \"arbitrary\")")
  1395 
  1395 
  1396 end
  1396 end