src/HOL/Library/Char_ord.thy
changeset 21911 e29bcab0c81c
parent 21871 9ce66839d9f1
child 22483 86064f2f2188
     1.1 --- a/src/HOL/Library/Char_ord.thy	Wed Dec 27 19:09:59 2006 +0100
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Wed Dec 27 19:10:00 2006 +0100
     1.3 @@ -98,6 +98,7 @@
     1.4  
     1.5  code_const char_to_int_pair
     1.6    (SML "raise/ Fail/ \"char'_to'_int'_pair\"")
     1.7 +  (OCaml "failwith \"char'_to'_int'_pair\"")
     1.8    (Haskell "error/ \"char'_to'_int'_pair\"")
     1.9  
    1.10  end