diff -r dc65319809cc -r 80dabcaafc38 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Tue Mar 02 14:51:40 2010 +0100
+++ b/Nominal/Rsp.thy	Tue Mar 02 15:10:47 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