--- a/Nominal/NewParser.thy	Fri Apr 30 10:04:24 2010 +0200
+++ b/Nominal/NewParser.thy	Fri Apr 30 10:31:32 2010 +0200
@@ -277,8 +277,9 @@
   val thy = Local_Theory.exit_global lthy2;
   val lthy3 = Theory_Target.init NONE thy;
 
-  val ((fv, fvbn), info, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
-  val (alpha, lthy5) = define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy4;
+  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;
 in
   ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy5)
 end