src/HOL/Nominal/nominal_inductive.ML

                      map (fold (NominalPackage.mk_perm []) pis') (tl ts))))
                    (fn _ => EVERY ([simp_tac eqvt_ss 1, rtac ihyp' 1,
                      REPEAT_DETERM_N (nprems_of ihyp - length gprems)
                        (simp_tac swap_simps_ss 1),
                      REPEAT_DETERM_N (length gprems)
-                       (simp_tac (HOL_ss
-                          addsimps inductive_forall_def' :: gprems2
-                          addsimprocs [NominalPackage.perm_simproc]) 1)]));
+                       (simp_tac (HOL_basic_ss
+                          addsimps [inductive_forall_def']
+                          addsimprocs [NominalPackage.perm_simproc]) 1 THEN
+                        resolve_tac gprems2 1)]));
                  val final = Goal.prove ctxt'' [] [] (term_of concl)
                    (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (HOL_ss
                      addsimps vc_compat_ths'' @ freshs2' @
                        perm_fresh_fresh @ fresh_atm) 1);
                  val final' = ProofContext.export ctxt'' ctxt' [final];