author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
Wed, 14 Apr 2010 20:21:11 +0200 | |
changeset 1844 | c123419a4eb0 |
parent 1843 | 35e06fc27744 (diff) |
parent 1842 | 2a61e91019a3 (current diff) |
child 1845 | b7423c6b5564 |
--- 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;