--- a/Nominal-General/Nominal2_Eqvt.thy	Fri Apr 16 11:09:32 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Fri Apr 16 16:29:11 2010 +0200
@@ -369,6 +369,7 @@
 
 text {* Problem: there is no raw eqvt-rule for The *}
 lemma "p \<bullet> (THE x. P x) = foo"
+apply(tactic {* Nominal_Permeq.eqvt_tac @{context} [] [@{const_name "The"}] 1*})
 apply(perm_simp)
 (* apply(perm_strict_simp) *)
 oops

--- a/Nominal-General/nominal_eqvt.ML	Fri Apr 16 11:09:32 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Fri Apr 16 16:29:11 2010 +0200
@@ -86,22 +86,28 @@
 
 (** equivariance tactics **)
 
+val perm_boolE = @{thm permute_boolE}
+val perm_cancel = @{thms permute_minus_cancel(2)}
+val perm_expand_bool = @{thms permute_fun_def minus_minus permute_bool_def}
+
 fun eqvt_rel_case_tac ctxt pred_names pi intro  = 
 let
   val thy = ProofContext.theory_of ctxt
   val cpi = Thm.cterm_of thy (mk_minus pi)
-  val rule = Drule.instantiate' [] [SOME cpi] @{thm permute_boolE}
-  val permute_cancel = @{thms permute_minus_cancel(2)}
+  val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE
+  val simps = HOL_basic_ss addsimps perm_expand_bool
 in
-  eqvt_strict_tac ctxt [] [] THEN' 
-  SUBPROOF (fn {prems, context, ...} =>
+  eqvt_strict_tac ctxt [] pred_names THEN' 
+  SUBPROOF (fn {prems, context as ctxt, ...} =>
     let
       val prems' = map (transform_prem ctxt pred_names) prems
-      val side_cond_tac = EVERY' 
-        [ rtac rule, eqvt_strict_tac context permute_cancel [],
-          resolve_tac prems' ]
+      val tac1 = resolve_tac prems'
+      val tac2 = EVERY' [ rtac pi_intro_rule, 
+            eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ]
+      val tac3 = EVERY' [ rtac pi_intro_rule, 
+            eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps, resolve_tac prems']
     in
-      (rtac intro THEN_ALL_NEW (resolve_tac prems' ORELSE' side_cond_tac)) 1 
+      (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 
     end) ctxt
 end
 

--- a/Nominal-General/nominal_permeq.ML	Fri Apr 16 11:09:32 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Fri Apr 16 16:29:11 2010 +0200
@@ -106,11 +106,16 @@
 
 (* conversion that raises an error or prints a warning message, 
    if a permutation on a constant or application cannot be analysed *)
-fun progress_info_conv ctxt strict_flag ctrm =
+fun progress_info_conv ctxt strict_flag bad_hds ctrm =
 let
-  fun msg trm = 
-    (if strict_flag then error else warning) 
-      ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
+  fun msg trm =
+    let
+      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))
+    end
 
   val _ = case (term_of ctrm) of
       Const (@{const_name "permute"}, _) $ _ $ (trm as Const _) => msg trm
@@ -136,7 +141,7 @@
       eqvt_apply_conv bad_hds,
       eqvt_lambda_conv,
       More_Conv.rewrs_conv post_thms,
-      progress_info_conv ctxt strict_flag
+      progress_info_conv ctxt strict_flag bad_hds
     ] ctrm
 end
 

--- a/Nominal/Ex/Classical.thy	Fri Apr 16 11:09:32 2010 +0200
+++ b/Nominal/Ex/Classical.thy	Fri Apr 16 16:29:11 2010 +0200
@@ -63,6 +63,14 @@
    alpha (ImpR_raw coname1 name trm_raw coname2)
          (ImpR_raw coname1a namea trm_rawa coname2a)"
 
+thm alpha.intros
+
+declare permute_trm_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+
+equivariance alpha
+thm eqvts_raw
+
 
 end
 

--- a/Nominal/Ex/Lambda.thy	Fri Apr 16 11:09:32 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Fri Apr 16 16:29:11 2010 +0200
@@ -188,56 +188,28 @@
 
 declare permute_lam_raw.simps[eqvt]
 declare alpha_gen_eqvt[eqvt]
-(*equivariance alpha_lam_raw'*)
+equivariance alpha_lam_raw'
 thm eqvts_raw
 
+
+
+(* HERE *)
+
 lemma
   assumes a: "alpha_lam_raw' t1 t2"
   shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)"
 using a
 apply(induct)
-apply(perm_simp)
-apply(rule a1)
-apply(simp)
-apply(perm_simp)
-apply(rule a2)
-apply(simp)
-apply(simp)
-
-apply simp
-apply (rule a3)
-apply (erule exi[of _ _ "p"])
-apply (simp add: alphas)
-apply (erule conjE)+
-apply (rule conjI)
-apply (rule permute_eq_iff[of "- p", THEN iffD1])
-apply (simp add: eqvts)
-apply (rule conjI)
-apply (rule fresh_star_permute_iff[of "- p", THEN iffD1])
-apply (simp add: eqvts)
-apply (rule conjI)
-apply (simp add: permute_eqvt[symmetric])
-apply (rule permute_eq_iff[of "- p", THEN iffD1])
-apply (subst permute_eqvt)
-apply (simp add: eqvts)
-done
-
-lemma
-  assumes a: "alpha_lam_raw' t1 t2"
-  shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)"
-using a
-apply(induct)
-ML_prf {*
-val ({names, ...}, {raw_induct, intrs, ...}) =
-    Inductive.the_inductive @{context} (Sign.intern_const @{theory} "alpha_lam_raw")
-*}
+apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
+  @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a1} 1*})
 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
-  @{context} ["Lambda.alpha_lam_raw"] @{term "p::perm"} @{thm a1} 1*})
+  @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a2} 1*})
+(*
 apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
-  @{context} ["Lambda.alpha_lam_raw"] @{term "p::perm"} @{thm a2} 1*})
+  @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a3} 1*})
+*)
 oops
 
-
 section {* size function *}
 
 lemma size_eqvt_raw: