--- a/src/HOL/List.thy Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/List.thy Sat Jan 25 23:50:49 2014 +0100
@@ -6318,14 +6318,14 @@
fun implode_list nil' cons' t =
let
- fun dest_cons (IConst { name = c, ... } `$ t1 `$ t2) =
+ fun dest_cons (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
if c = cons'
then SOME (t1, t2)
else NONE
| dest_cons _ = NONE;
val (ts, t') = Code_Thingol.unfoldr dest_cons t;
in case t'
- of IConst { name = c, ... } => if c = nil' then SOME ts else NONE
+ of IConst { sym = Code_Symbol.Constant c, ... } => if c = nil' then SOME ts else NONE
| _ => NONE
end;