diff -r b0eae8c93314 -r da44ef9a7df2 Nominal/Lift.thy
--- a/Nominal/Lift.thy	Tue Mar 02 16:03:19 2010 +0100
+++ b/Nominal/Lift.thy	Tue Mar 02 16:04:48 2010 +0100
@@ -82,7 +82,6 @@
 val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) nos
 val typs = List.take (all_typs, number)
 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
-val full_tnames = List.take (all_full_tnames, number);
 val induct = #induct info;
 val inducts = #inducts info;
 val infos = map (Datatype.the_info thy1) all_full_tnames;
@@ -106,10 +105,7 @@
 val morphism = ProofContext.export_morphism lthy2 lthy1
 val fv_ts = map (Morphism.term morphism) fv_ts_loc
 val alpha_ts = map (Morphism.term morphism) alpha_ts_loc
-fun build_bv_eqvt (t, n) =
-  build_eqvts Binding.empty [t] [nth perms n]
-    (bv_simps @ raw_perm_def) (nth inducts n)
-val (bv_eqvts, lthy3) = fold_map build_bv_eqvt bvs lthy2;
+val (bv_eqvts, lthy3) = fold_map (build_bv_eqvt perms (bv_simps @ raw_perm_def) inducts)  bvs lthy2;
 val (fv_eqvts, lthy4) = build_eqvts Binding.empty fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3;
 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy4;
 val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_loc;