--- a/Nominal-General/nominal_permeq.ML	Tue May 04 17:25:58 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Wed May 05 10:24:54 2010 +0100
@@ -97,7 +97,7 @@
         val term_insts = map SOME [p, f, x]                        
       in
         if has_bad_head bad_hds trm
-        then Conv.no_conv ctrm
+        then Conv.all_conv ctrm
         else Drule.instantiate' ty_insts term_insts @{thm eqvt_apply}
       end
   | _ => Conv.no_conv ctrm
@@ -115,11 +115,11 @@
 let
   fun msg trm =
     let
-      val hd = head_of trm 
+      val hd = head_of trm
     in 
-    if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then ()
-    else (if strict_flag then error else warning) 
-           ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
+      if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then ()
+      else (if strict_flag then error else warning) 
+             ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
     end
 
   val _ = case (term_of ctrm) of
@@ -130,7 +130,7 @@
   Conv.all_conv ctrm 
 end
 
-(* main conversion *)
+(* main conversion *) 
 fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm =
 let
   val first_conv_wrapper = 
@@ -150,13 +150,19 @@
     ] ctrm
 end
 
+(* the eqvt-tactics first eta-normalise goals in 
+   order to avoid problems with inductions in the
+   equivaraince command. *)
+
 (* raises an error if some permutations cannot be eliminated *)
 fun eqvt_strict_tac ctxt user_thms bad_hds = 
-  CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt true user_thms bad_hds) ctxt)
+  CONVERSION (More_Conv.top_conv 
+    (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt true user_thms bad_hds)) ctxt)
 
 (* prints a warning message if some permutations cannot be eliminated *)
 fun eqvt_tac ctxt user_thms bad_hds = 
-  CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt false user_thms bad_hds) ctxt)
+  CONVERSION (More_Conv.top_conv 
+    (fn ctxt => Thm.eta_conversion then_conv (eqvt_conv ctxt false user_thms bad_hds)) ctxt)
 
 (* setup of the configuration value *)
 val setup =
@@ -169,9 +175,7 @@
 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- 
   (Scan.repeat (Args.const true))) []
 
-val args_parser =  
-  add_thms_parser -- exclude_consts_parser ||
-  exclude_consts_parser -- add_thms_parser >> swap
+val args_parser =  add_thms_parser -- exclude_consts_parser 
 
 fun perm_simp_meth (thms, consts) ctxt = 
   SIMPLE_METHOD (HEADGOAL (eqvt_tac ctxt thms consts))