src/HOL/Tools/datatype_rep_proofs.ML

     val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
 
     val dt_induct_prop = DatatypeProp.make_ind descr sorts;
     val dt_induct = SkipProof.prove_global thy6 []
       (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
-      (fn prems => EVERY
+      (fn {prems, ...} => EVERY
         [rtac indrule_lemma' 1,
          (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
          EVERY (map (fn (prem, r) => (EVERY
            [REPEAT (eresolve_tac Abs_inverse_thms 1),
             simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,