--- a/Nominal/Lift.thy	Wed Apr 14 16:11:04 2010 +0200
+++ b/Nominal/Lift.thy	Wed Apr 14 20:20:54 2010 +0200
@@ -71,9 +71,8 @@
 let
   val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') =
     define_fv dt binds bns ctxt;
-  val fv_ts_nobn = take (length bns) fv_ts_loc
   val (alpha, ctxt'') =
-    define_alpha dt binds bns fv_ts_nobn ctxt';
+    define_alpha dt binds bns fv_ts_loc ctxt';
   val alpha_ts_loc = #preds alpha
   val alpha_induct_loc = #induct alpha
   val alpha_intros_loc = #intrs alpha;