src/HOL/Nominal/nominal_atoms.ML

 structure NominalAtoms : NOMINAL_ATOMS =
 struct
 
 val finite_emptyI = @{thm "finite.emptyI"};
 val Collect_const = @{thm "Collect_const"};
+
+val inductive_forall_def = @{thm "induct_forall_def"};
 
 
 (* theory data *)
 
 type atom_info =

             ||>> PureThy.add_thmss [(("perm_compose'",inst_pt_at [pt_perm_compose']),[])] 
             ||>> PureThy.add_thmss [(("perm_app", inst_pt_at [perm_app]),[])]
             ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
             ||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
             ||>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])]
-            ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[NominalThmDecls.eqvt_force_add])] 
+            ||>> PureThy.add_thmss
+              let
+                val thms1 = inst_pt_at [all_eqvt];
+                val thms2 = map (fold_rule [inductive_forall_def]) thms1
+              in
+                [(("all_eqvt", thms1 @ thms2), [NominalThmDecls.eqvt_force_add])]
+              end
             ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_force_add])]
             ||>> PureThy.add_thmss 
 	      let val thms1 = inst_at [at_fresh]
 		  val thms2 = inst_dj [at_fresh_ineq]
 	      in [(("fresh_atm", thms1 @ thms2),[])] end