src/HOL/Nominal/nominal_atoms.ML
changeset 22715 381e6c45f13b
parent 22611 0e008e3ddb1e
child 22745 17bc6af2011e
--- a/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 16 06:45:22 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Apr 16 07:32:23 2007 +0200
@@ -802,8 +802,8 @@
             ||>> 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_add])] 
-            ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_add])]
+            ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[NominalThmDecls.eqvt_force_add])] 
+            ||>> 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]