src/HOL/Tools/datatype_package.ML

 
     fun err t = error ("Ill-formed predicate in induction rule: " ^
       Sign.string_of_term thy1 t);
 
     fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
-          ((tname, map dest_TFree Ts) handle TERM _ => err t)
+          ((tname, map (fst o dest_TFree) Ts) handle TERM _ => err t)
       | get_typ t = err t;
 
     val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induction')));
     val new_type_names = getOpt (alt_names, map fst dtnames);