diff -r 72ad4e766acf -r 8aff3f3ce47f Nominal/NewAlpha.thy
--- a/Nominal/NewAlpha.thy	Sat May 22 13:51:47 2010 +0100
+++ b/Nominal/NewAlpha.thy	Sun May 23 02:15:24 2010 +0100
@@ -127,7 +127,7 @@
 let
   fun mk_alphabn_free (bn, ith, _) =
     let
-      val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Free bn)));
+      val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));
       val ty = nth_dtyp dt_descr sorts ith;
       val alphabn_type = ty --> ty --> @{typ bool};
       val alphabn_free = Free(alphabn_name, alphabn_type);
@@ -190,10 +190,8 @@
 *}
 
 ML {*
-fun define_raw_alpha (dt_info : Datatype_Aux.info) bn_funs bclausesss fv_frees lthy =
+fun define_raw_alpha dt_descr sorts bn_funs bclausesss fv_frees lthy =
 let
-  val {descr as dt_descr, sorts, ...} = dt_info;
-
   val alpha_names = prefix_dt_names dt_descr sorts "alpha_";
   val alpha_types = map (fn (i, _) =>
     nth_dtyp dt_descr sorts i --> nth_dtyp dt_descr sorts i --> @{typ bool}) dt_descr;
@@ -230,8 +228,9 @@
   val alpha_intros = Morphism.fact morphism alpha_intros_loc
   val alpha_cases = Morphism.fact morphism alpha_cases_loc
 in
-  (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy')
+  (alpha_ts, alpha_intros, alpha_cases, alpha_induct, lthy')
 end
+handle UnequalLengths => error "Main"
 *}
 
 end