--- a/Nominal/Lift.thy Tue Mar 02 15:10:47 2010 +0100
+++ b/Nominal/Lift.thy Tue Mar 02 15:11:41 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;