--- a/Nominal/Rsp.thy	Wed Mar 24 09:59:47 2010 +0100
+++ b/Nominal/Rsp.thy	Wed Mar 24 10:49:50 2010 +0100
@@ -212,11 +212,6 @@
 *}
 
 ML {*
-fun build_bv_eqvt simps inducts (t, n) ctxt =
-  build_eqvts Binding.empty [t] (build_eqvts_tac (nth inducts n) simps ctxt) ctxt
-*}
-
-ML {*
 fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt =
 let
   val (fvs_alphas, ls) = split_list fv_alphas_lst;