src/HOL/List.thy
changeset 55147 bce3dbc11f95
parent 55129 26bd1cba3ab5
child 55148 7e1b7cb54114
     1.1 --- a/src/HOL/List.thy	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/HOL/List.thy	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -6318,14 +6318,14 @@
     1.4  
     1.5  fun implode_list nil' cons' t =
     1.6    let
     1.7 -    fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
     1.8 +    fun dest_cons (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
     1.9            if c = cons'
    1.10            then SOME (t1, t2)
    1.11            else NONE
    1.12        | dest_cons _ = NONE;
    1.13      val (ts, t') = Code_Thingol.unfoldr dest_cons t;
    1.14    in case t'
    1.15 -   of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
    1.16 +   of IConst { sym = Code_Symbol.Constant c, ... } => if c = nil' then SOME ts else NONE
    1.17      | _ => NONE
    1.18    end;
    1.19