--- a/Nominal/nominal_dt_alpha.ML	Wed Jul 06 15:59:11 2011 +0200
+++ b/Nominal/nominal_dt_alpha.ML	Thu Jul 07 16:16:42 2011 +0200
@@ -9,8 +9,8 @@
 sig
   val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term
 
-  val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> 
-    bclause list list list -> term list -> Proof.context -> alpha_result * local_theory
+  val define_raw_alpha: raw_dt_info -> bn_info list -> bclause list list list -> term list -> 
+    Proof.context -> alpha_result * local_theory
 
   val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> 
     (Proof.context -> int -> tactic) -> Proof.context -> thm list
@@ -18,8 +18,8 @@
   val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> 
     (Proof.context -> int -> tactic) -> Proof.context -> thm list
 
-  val raw_prove_alpha_distincts: Proof.context -> alpha_result -> thm list -> string list -> thm list
-  val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> thm list -> thm list -> thm list
+  val raw_prove_alpha_distincts: Proof.context -> alpha_result -> raw_dt_info -> thm list
+  val raw_prove_alpha_eq_iff: Proof.context -> alpha_result -> raw_dt_info -> thm list
   val raw_prove_refl: Proof.context -> alpha_result -> thm -> thm list
   val raw_prove_sym: Proof.context -> alpha_result -> thm list -> thm list
   val raw_prove_trans: Proof.context -> alpha_result -> thm list -> thm list -> thm list
@@ -224,9 +224,11 @@
     map2 (mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
   end
 
-fun define_raw_alpha raw_full_ty_names raw_tys cns_info bn_info bclausesss fvs lthy =
+fun define_raw_alpha raw_dt_info bn_info bclausesss fvs lthy =
   let
-    val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_full_ty_names
+    val RawDtInfo {raw_dt_names, raw_tys, raw_cns_info, ...} = raw_dt_info
+
+    val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_dt_names
     val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) raw_tys
     val alpha_frees = map Free (alpha_names ~~ alpha_tys)
     val alpha_map = raw_tys ~~ (alpha_frees ~~ fvs)
@@ -239,8 +241,8 @@
     val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys)
     val alpha_bn_map = bns ~~ alpha_bn_frees
 
-    val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) cns_info bclausesss 
-    val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map cns_info bclausesss) bn_info
+    val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) raw_cns_info bclausesss 
+    val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map raw_cns_info bclausesss) bn_info
 
     val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn))
       (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
@@ -393,9 +395,10 @@
   rtac notI THEN' eresolve_tac cases_thms 
   THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms)
 
-fun raw_prove_alpha_distincts ctxt alpha_result raw_distinct_thms raw_dt_names =
+fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info =
   let
     val AlphaResult {alpha_names, alpha_cases, ...} = alpha_result
+    val RawDtInfo {raw_dt_names, raw_distinct_thms, ...} = raw_dt_info
 
     val ty_trm_assoc = raw_dt_names ~~ alpha_names
 
@@ -439,9 +442,10 @@
     else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps))
   end;
 
-fun raw_prove_alpha_eq_iff ctxt alpha_result raw_distinct_thms raw_inject_thms =
+fun raw_prove_alpha_eq_iff ctxt alpha_result raw_dt_info =
   let
     val AlphaResult {alpha_intros, alpha_cases, ...} = alpha_result
+    val RawDtInfo {raw_distinct_thms, raw_inject_thms, ...} = raw_dt_info
 
     val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt;
     val goals = map mk_alpha_eq_iff_goal thms_imp;