diff -r f03bfddc5aea -r 4df3441aa0b4 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Fri Apr 30 10:48:48 2010 +0200
+++ b/Nominal/NewParser.thy	Fri Apr 30 13:57:59 2010 +0200
@@ -267,6 +267,15 @@
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
   val {descr, sorts, ...} = dtinfo;
 
+  val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
+  val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames;
+  val inject = flat (map #inject dtinfos);
+  val distincts = flat (map #distinct dtinfos);
+  val rel_dtinfos = List.take (dtinfos, (length dts));
+  val rel_distinct = map #distinct rel_dtinfos;
+  val induct = #induct dtinfo;
+  val exhausts = map #exhaust dtinfos;
+
   val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1;
 
@@ -277,11 +286,13 @@
   val thy = Local_Theory.exit_global lthy2;
   val lthy3 = Theory_Target.init NONE thy;
 
-  val ((fv, fvbn), fvsimps, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
-  val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy5) =
-    define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy4;
+  val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
+  val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
+    define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a;
+  val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
+
 in
-  ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy5)
+  ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy4)
 end
 *}
 
@@ -468,7 +479,7 @@
 | "bn (P2 p1 p2) = bn p1 \<union> bn p2"
 
 thm fv_lam_raw.simps fv_pt_raw.simps fv_bn_raw.simps
-thm alpha_lam_raw_alpha_pt_raw_alpha_bn_raw.intros
+thm alpha_lam_raw_alpha_pt_raw_alpha_bn_raw.intros[no_vars]
 
 nominal_datatype exp =
   EVar name