diff -r cf79f8866bc3 -r b3f2b8c906a6 src/HOL/Library/Code_Test.thy --- a/src/HOL/Library/Code_Test.thy Fri Mar 11 17:20:14 2016 +0100 +++ b/src/HOL/Library/Code_Test.thy Sat Mar 12 22:04:52 2016 +0100 @@ -83,8 +83,8 @@ definition list where "list f xs = map (node \ f) xs" -definition X :: yxml_of_term where "X = yot_literal (STR [Char Nibble0 Nibble5])" -definition Y :: yxml_of_term where "Y = yot_literal (STR [Char Nibble0 Nibble6])" +definition X :: yxml_of_term where "X = yot_literal (STR [Char (num.Bit1 (num.Bit0 num.One))])" +definition Y :: yxml_of_term where "Y = yot_literal (STR [Char (num.Bit0 (num.Bit1 num.One))])" definition XY :: yxml_of_term where "XY = yot_append X Y" definition XYX :: yxml_of_term where "XYX = yot_append XY X"