--- a/Nominal-General/Nominal2_Eqvt.thy	Sun Apr 11 18:06:45 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sun Apr 11 18:08:57 2010 +0200
@@ -248,7 +248,7 @@
 
   (* datatypes *)
   permute_prod.simps append_eqvt rev_eqvt set_eqvt
-  fst_eqvt snd_eqvt Pair_eqvt
+  fst_eqvt snd_eqvt Pair_eqvt permute_list.simps
 
   (* sets *)
   empty_eqvt UNIV_eqvt union_eqvt inter_eqvt mem_eqvt

--- a/Nominal-General/nominal_permeq.ML	Sun Apr 11 18:06:45 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Sun Apr 11 18:08:57 2010 +0200
@@ -47,7 +47,7 @@
   val lhs_str = Syntax.string_of_term ctxt (term_of (Thm.lhs_of result))
   val rhs_str = Syntax.string_of_term ctxt (term_of (Thm.rhs_of result))
 in
-  tracing (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str]))
+  warning (Pretty.string_of (Pretty.strs ["Rewriting", lhs_str, "to", rhs_str]))
 end
 
 fun trace_conv ctxt conv ctrm =
@@ -66,7 +66,7 @@
   val trm = term_of ctrm
   val _ = case (head_of trm) of 
       @{const "Trueprop"} => ()
-    | _ => tracing ("Analysing term " ^ Syntax.string_of_term ctxt trm)
+    | _ => warning ("Analysing term " ^ Syntax.string_of_term ctxt trm)
 in
   Conv.no_conv ctrm
 end
@@ -121,16 +121,18 @@
   Conv.all_conv ctrm 
 end
 
+fun mk_equiv r = r RS @{thm eq_reflection};
+fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
 
 (* main conversion *)
-fun eqvt_conv ctxt strict_flag thms bad_hds ctrm =
+fun eqvt_conv ctxt strict_flag user_thms bad_hds ctrm =
 let
   val first_conv_wrapper = 
     if trace_enabled ctxt 
     then Conv.first_conv o (cons (trace_info_conv ctxt)) o (map (trace_conv ctxt))
     else Conv.first_conv
 
-  val pre_thms = thms @ @{thms eqvt_bound} @ (get_eqvts_raw_thms ctxt)
+  val pre_thms = (map safe_mk_equiv user_thms) @ @{thms eqvt_bound} @ (get_eqvts_raw_thms ctxt)
   val post_thms = @{thms permute_pure[THEN eq_reflection]}
 in
   first_conv_wrapper
@@ -143,12 +145,12 @@
 end
 
 (* raises an error if some permutations cannot be eliminated *)
-fun eqvt_strict_tac ctxt thms bad_hds = 
-  CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt true thms bad_hds) ctxt)
+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)
 
 (* prints a warning message if some permutations cannot be eliminated *)
-fun eqvt_tac ctxt thms bad_hds = 
-  CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt false thms bad_hds) ctxt)
+fun eqvt_tac ctxt user_thms bad_hds = 
+  CONVERSION (More_Conv.top_conv (fn ctxt => eqvt_conv ctxt false user_thms bad_hds) ctxt)
 
 (* setup of the configuration value *)
 val setup =