--- a/Nominal-General/Nominal2_Eqvt.thy	Fri Apr 09 21:51:01 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sun Apr 11 10:36:09 2010 +0200
@@ -282,15 +282,19 @@
   shows "p \<bullet> unpermute p x \<equiv> x"
   unfolding unpermute_def by simp
 
-ML {* @{const Trueprop} *}
-
 use "nominal_permeq.ML"
 setup Nominal_Permeq.setup
 
 method_setup perm_simp =
- {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms))) *}
+ {* Attrib.thms >> 
+    (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_tac ctxt thms ["The"]))) *}
  {* pushes permutations inside *}
 
+method_setup perm_strict_simp =
+ {* Attrib.thms >> 
+    (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Nominal_Permeq.eqvt_strict_tac ctxt thms ["The"]))) *}
+ {* pushes permutations inside, raises an error if it cannot solve all permutations *}
+
 declare [[trace_eqvt = true]]
 
 lemma 
@@ -352,13 +356,6 @@
 oops
 
 lemma 
-  fixes p q r::"perm"
-  and   x::"'a::pt"
-  shows "p \<bullet> (q \<bullet> r \<bullet> x) = foo"
-apply(perm_simp)
-oops
-
-lemma 
   fixes C D::"bool"
   shows "B (p \<bullet> (C = D))"
 apply(perm_simp)
@@ -369,6 +366,7 @@
 text {* Problem: there is no raw eqvt-rule for The *}
 lemma "p \<bullet> (THE x. P x) = foo"
 apply(perm_simp)
+(* apply(perm_strict_simp) *)
 oops