diff -r 9909cc3566c5 -r 636de31888a6 Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Wed Apr 14 15:02:07 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Wed Apr 14 16:05:58 2010 +0200
@@ -285,12 +285,10 @@
   shows "p \<bullet> unpermute p x \<equiv> x"
   unfolding unpermute_def by simp
 
+(* provides perm_simp methods *)
 use "nominal_permeq.ML"
 setup Nominal_Permeq.setup
 
-use "nominal_eqvt.ML"
-
-
 method_setup perm_simp =
  {* Attrib.thms >> 
     (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms ["The"]))) *}
@@ -375,6 +373,8 @@
 (* apply(perm_strict_simp) *)
 oops
 
-
+(* automatic equivariance procedure for 
+   inductive definitions *)
+use "nominal_eqvt.ML"
 
 end