--- a/Nominal/nominal_dt_alpha.ML	Mon May 24 20:50:15 2010 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Mon May 24 21:11:33 2010 +0100
@@ -9,7 +9,7 @@
 sig
   val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
     bclause list list list -> term list -> Proof.context -> 
-    term list * thm list * thm list * thm * local_theory
+    term list * term list * thm list * thm list * thm * local_theory
 end
 
 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
@@ -219,18 +219,20 @@
       coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
      all_alpha_names [] all_alpha_intros [] lthy
 
-  val alpha_trms_loc = #preds alphas;
+  val all_alpha_trms_loc = #preds alphas;
   val alpha_induct_loc = #raw_induct alphas;
   val alpha_intros_loc = #intrs alphas;
   val alpha_cases_loc = #elims alphas;
   val phi = ProofContext.export_morphism lthy' lthy;
 
-  val alpha_trms = map (Morphism.term phi) alpha_trms_loc;
+  val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc;
   val alpha_induct = Morphism.thm phi alpha_induct_loc;
   val alpha_intros = map (Morphism.thm phi) alpha_intros_loc
   val alpha_cases = map (Morphism.thm phi) alpha_cases_loc
+
+  val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms
 in
-  (alpha_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
+  (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
 end
 
 end (* structure *)