src/HOL/Tools/typecopy.ML

   let
     val ty = Sign.certify_typ thy raw_ty;
     val vs =
       AList.make (the_default HOLogic.typeS o AList.lookup (op =) (Term.add_tfreesT ty [])) raw_vs;
     val tac = Tactic.rtac UNIV_witness 1;
-    fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
-      Rep_name = c_rep, Abs_inject = inject,
-      Abs_inverse = inverse, ... } : Typedef.info ) thy =
+    fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
+          Rep_name = c_rep, ...}, { Abs_inject = inject, Abs_inverse = inverse, ... })
+          : Typedef.info) thy =
         let
           val exists_thm =
             UNIV_I
             |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global ty_rep))] [];
           val inject' = inject OF [exists_thm, exists_thm];

 fun add_default_code tyco thy =
   let
     val SOME { constr = c, proj = (proj, _), proj_def = proj_eq, vs = vs,
       typ = ty_rep, ... } = get_info thy tyco;
     (* FIXME handle multiple typedef interpretations (!??) *)
-    val [{ Rep_inject = proj_inject, ... }] = Typedef.get_info_global thy tyco;
+    val [(_, { Rep_inject = proj_inject, ... })] = Typedef.get_info_global thy tyco;
     val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c));
     val ty = Type (tyco, map TFree vs);
     val proj = Const (proj, ty --> ty_rep);
     val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));
     val eq_lhs = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)