# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271269254 -7200
# Node ID 35e06fc277442facb8762a7786c5f079e6b9661f
# Parent  b435ee87d9c8728504af2c6ad863aeb161c95656
Fix the 'subscript' error.

diff -r b435ee87d9c8 -r 35e06fc27744 Nominal/Lift.thy
--- 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;