src/HOL/Tools/Lifting/lifting_def_code_dt.ML

       |> Local_Theory.end_nested
 
     (* in order to make the qty qty_isom isomorphism executable we have to define discriminators 
       and selectors for qty_isom *)
     val (rty_name, typs) = dest_Type rty
-    val (_, qty_typs) = dest_Type qty
+    val qty_typs = dest_Type_args qty
     val fp = BNF_FP_Def_Sugar.fp_sugar_of lthy3 rty_name
     val fp = if is_some fp then the fp
       else error ("code_dt: " ^ quote rty_name ^ " is not a datatype.")
     val ctr_sugar = fp |> #fp_ctr_sugar |> #ctr_sugar
     val ctrs = map (Ctr_Sugar.mk_ctr typs) (#ctrs ctr_sugar);