diff -r 5335c0ea743a -r 313e6f2cdd89 Nominal/nominal_permeq.ML
--- a/Nominal/nominal_permeq.ML	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/nominal_permeq.ML	Mon Jun 04 21:39:51 2012 +0100
@@ -18,6 +18,7 @@
   val delpres : eqvt_config -> eqvt_config
   val delposts : eqvt_config -> eqvt_config
 
+  val eqvt_conv: Proof.context -> eqvt_config -> conv 
   val eqvt_rule: Proof.context -> eqvt_config -> thm -> thm
   val eqvt_tac: Proof.context -> eqvt_config -> int -> tactic