merge
authorCezary 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
merge
--- 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;