# HG changeset patch # User haftmann # Date 1241629754 -7200 # Node ID b7e1c065b6e41e5bd1b6eb62cfd3b66fbbb857f2 # Parent 9a3bd9dbdd0ff0561dd0f0b3a7817cd9a83c1258 confine term setup to Eval serialiser diff -r 9a3bd9dbdd0f -r b7e1c065b6e4 src/HOL/Library/Code_Char.thy --- a/src/HOL/Library/Code_Char.thy Wed May 06 16:10:12 2009 +0200 +++ b/src/HOL/Library/Code_Char.thy Wed May 06 19:09:14 2009 +0200 @@ -14,8 +14,8 @@ (Haskell "Char") setup {* - fold (fn target => add_literal_char target) ["SML", "OCaml", "Haskell"] - #> add_literal_list_string "Haskell" + fold String_Code.add_literal_char ["SML", "OCaml", "Haskell"] + #> String_Code.add_literal_list_string "Haskell" *} code_instance char :: eq