src/HOL/Library/Code_Test.thy
changeset 68028 1f9f973eed2a
parent 67443 3abf6a722518
child 68033 ad4b8b6892c3
--- a/src/HOL/Library/Code_Test.thy	Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Library/Code_Test.thy	Tue Apr 24 14:17:58 2018 +0000
@@ -84,8 +84,8 @@
 
 definition list where "list f xs = map (node \<circ> f) xs"
 
-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 X :: yxml_of_term where "X = yot_literal (ASCII 0x05)"
+definition Y :: yxml_of_term where "Y = yot_literal (ASCII 0x06)"
 definition XY :: yxml_of_term where "XY = yot_append X Y"
 definition XYX :: yxml_of_term where "XYX = yot_append XY X"