# HG changeset patch
# User haftmann
# Date 1517649081 0
# Node ID 3817a93a3e5e3299bec5096b9658ca0fcf8287f3
# Parent  37ba3d234fbfd9ce15a6af9d7b9f733ddd7d0e26
special treatment of 0 only refers to type char

diff -r 37ba3d234fbf -r 3817a93a3e5e src/HOL/Tools/string_code.ML
--- a/src/HOL/Tools/string_code.ML	Fri Feb 16 14:41:20 2018 +0100
+++ b/src/HOL/Tools/string_code.ML	Sat Feb 03 09:11:21 2018 +0000
@@ -21,7 +21,7 @@
     SOME n => if 0 < n andalso n < 256 then SOME n else NONE
   | _ => NONE;
 
-fun decode_char (IConst { sym = Code_Symbol.Constant @{const_name Groups.zero}, ... }) =
+fun decode_char (IConst { sym = Code_Symbol.Constant @{const_name String.zero_char_inst.zero_char}, ... }) =
      SOME 0
   | decode_char (IConst { sym = Code_Symbol.Constant @{const_name Char}, ... } `$ t) =
       decode_char_nonzero t