src/HOL/HOLCF/Tools/Domain/domain_induction.ML

           EVERY (map finite_tac (take_induct_thms ~~ fin_inds))
         end
     in Goal.prove_global thy [] (adms @ assms) goal tacf end
 
   (* case names for induction rules *)
-  val dnames = map (fst o dest_Type) newTs
+  val dnames = map dest_Type_name newTs
   val case_ns =
     let
       val adms =
           if is_finite then [] else
           if length dnames = 1 then ["adm"] else