diff -r b452e11e409f -r 25b02cc185e2 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Thu Mar 11 10:22:24 2010 +0100
+++ b/Nominal/Rsp.thy	Thu Mar 11 10:39:29 2010 +0100
@@ -120,16 +120,17 @@
 *)
 
 ML {*
-fun build_eqvts bind funs perms simps induct ctxt =
+fun build_eqvts bind funs simps induct ctxt =
 let
   val pi = Free ("p", @{typ perm});
   val types = map (domain_type o fastype_of) funs;
   val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types));
   val args = map Free (indnames ~~ types);
   val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
-  fun eqvtc (fnctn, (arg, perm)) =
-    HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg)))
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))
+  fun perm_arg arg = Const (@{const_name permute}, @{typ perm} --> fastype_of arg --> fastype_of arg)
+  fun eqvtc (fnctn, arg) =
+    HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args)))
   fun tac _ = (Datatype_Aux.indtac induct indnames THEN_ALL_NEW
     (asm_full_simp_tac (HOL_ss addsimps
       (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1
@@ -195,8 +196,8 @@
 *}
 
 ML {*
-fun build_bv_eqvt perms simps inducts (t, n) =
-  build_eqvts Binding.empty [t] [nth perms n] simps (nth inducts n)
+fun build_bv_eqvt simps inducts (t, n) =
+  build_eqvts Binding.empty [t] simps (nth inducts n)
 *}
 
 end