# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271269271 -7200
# Node ID c123419a4eb01c86a7bdd271323cf113e179b94f
# Parent  35e06fc277442facb8762a7786c5f079e6b9661f# Parent  2a61e91019a35585b7d7bf380394a7ff7e665928
merge

diff -r 2a61e91019a3 -r c123419a4eb0 Nominal/Lift.thy
--- a/Nominal/Lift.thy	Wed Apr 14 18:47:20 2010 +0200
+++ b/Nominal/Lift.thy	Wed Apr 14 20:21:11 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;