--- a/Nominal-General/Nominal2_Eqvt.thy	Wed Apr 14 13:21:38 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Wed Apr 14 14:41:54 2010 +0200
@@ -9,6 +9,7 @@
 imports Nominal2_Base Nominal2_Atoms
 uses ("nominal_thmdecls.ML")
      ("nominal_permeq.ML")
+     ("nominal_eqvt.ML")
 begin
 
 
@@ -287,6 +288,9 @@
 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"]))) *}
@@ -371,4 +375,6 @@
 (* apply(perm_strict_simp) *)
 oops
 
+
+
 end