--- a/Nominal/Rsp.thy	Tue Mar 02 16:03:19 2010 +0100
+++ b/Nominal/Rsp.thy	Tue Mar 02 16:04:48 2010 +0100
@@ -175,4 +175,9 @@
 end
 *}
 
+ML {*
+fun build_bv_eqvt perms simps inducts (t, n) =
+  build_eqvts Binding.empty [t] [nth perms n] simps (nth inducts n)
+*}
+
 end