diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/Code_Char.thy --- a/src/HOL/Library/Code_Char.thy Fri Aug 27 15:36:02 2010 +0200 +++ b/src/HOL/Library/Code_Char.thy Fri Aug 27 19:34:23 2010 +0200 @@ -19,7 +19,7 @@ #> String_Code.add_literal_list_string "Haskell" *} -code_instance char :: eq +code_instance char :: equal (Haskell -) code_reserved SML @@ -31,7 +31,7 @@ code_reserved Scala char -code_const "eq_class.eq \ char \ char \ bool" +code_const "HOL.equal \ char \ char \ bool" (SML "!((_ : char) = _)") (OCaml "!((_ : char) = _)") (Haskell infixl 4 "==")