src/HOL/List.thy

 
 open Basic_Code_Thingol;
 
 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;
 
 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
   Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (