--- a/Nominal/Rsp.thy	Wed Mar 10 16:59:08 2010 +0100
+++ b/Nominal/Rsp.thy	Thu Mar 11 10:10:23 2010 +0100
@@ -176,7 +176,7 @@
 *}
 
 ML {*
-fun build_alpha_eqvts funs perms simps induct ctxt =
+fun build_alpha_eqvts funs perms tac ctxt =
 let
   val pi = Free ("p", @{typ perm});
   val types = map (domain_type o fastype_of) funs;
@@ -188,7 +188,6 @@
     HOLogic.mk_imp (alpha $ arg $ arg2,
       (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))
   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))
-  fun tac _ = alpha_eqvt_tac induct simps ctxt 1
   val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac
 in
   map (fn x => mp OF [x]) (HOLogic.conj_elims thm)