diff -r 4df3441aa0b4 -r f18b8e8a4909 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Fri Apr 30 13:57:59 2010 +0200
+++ b/Nominal/Parser.thy	Fri Apr 30 14:48:13 2010 +0200
@@ -391,8 +391,7 @@
     define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3;
   val (fv, fvbn) = chop (length perms) fv_ts;
 
-  val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts
-  val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct;
+  val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
   val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
@@ -476,7 +475,7 @@
     snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
   val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",
     [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13;
-  val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct
+  val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct
   val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
   val q_perm = map (lift_thm qtys lthy14) raw_perm_def;
   val lthy15 = note_simp_suffix "perm" q_perm lthy14a;