src/HOL/Tools/string_code.ML
changeset 48072 ace701efe203
parent 38923 79d7f2b4cf71
child 51160 599ff65b85e2
     1.1 --- a/src/HOL/Tools/string_code.ML	Mon Jun 04 12:55:54 2012 +0200
     1.2 +++ b/src/HOL/Tools/string_code.ML	Tue Jun 05 07:05:56 2012 +0200
     1.3 @@ -23,13 +23,13 @@
     1.4        | decode _ ~1 = NONE
     1.5        | decode n m = SOME (chr (n * 16 + m));
     1.6    in case tt
     1.7 -   of (IConst (c1, _), IConst (c2, _)) => decode (idx c1) (idx c2)
     1.8 +   of (IConst { name = c1, ... }, IConst { name = c2, ... }) => decode (idx c1) (idx c2)
     1.9      | _ => NONE
    1.10    end;
    1.11     
    1.12  fun implode_string char' nibbles' mk_char mk_string ts =
    1.13    let
    1.14 -    fun implode_char (IConst (c, _) `$ t1 `$ t2) =
    1.15 +    fun implode_char (IConst { name = c, ... } `$ t1 `$ t2) =
    1.16            if c = char' then decode_char nibbles' (t1, t2) else NONE
    1.17        | implode_char _ = NONE;
    1.18      val ts' = map_filter implode_char ts;