--- a/Nominal/nominal_dt_alpha.ML	Tue Aug 17 07:11:45 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Tue Aug 17 17:52:25 2010 +0800
@@ -7,9 +7,8 @@
 
 signature NOMINAL_DT_ALPHA =
 sig
-  val define_raw_alpha: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
-    bclause list list list -> term list -> Proof.context -> 
-    term list * term list * thm list * thm list * thm * local_theory
+  val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> 
+    term list -> Proof.context -> term list * term list * thm list * thm list * thm * local_theory
 
   val mk_alpha_distincts: Proof.context -> thm list -> thm list -> 
     term list -> typ list -> thm list
@@ -220,26 +219,23 @@
   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 descr sorts bn_info bclausesss fvs lthy =
+fun define_raw_alpha raw_full_ty_names raw_tys cns_info bn_info bclausesss fvs lthy =
 let
-  val alpha_names = prefix_dt_names descr sorts "alpha_"
-  val alpha_arg_tys = all_dtyps descr sorts
-  val alpha_tys = map (fn ty => [ty, ty] ---> @{typ bool}) alpha_arg_tys
+  val alpha_names = map (prefix "alpha_" o Long_Name.base_name) raw_full_ty_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 = alpha_arg_tys ~~ (alpha_frees ~~ fvs)
+  val alpha_map = raw_tys ~~ (alpha_frees ~~ fvs)
 
   val (bns, bn_tys) = split_list (map (fn (bn, i, _) => (bn, i)) bn_info)
   val bn_names = map (fn bn => Long_Name.base_name (fst (dest_Const bn))) bns
   val alpha_bn_names = map (prefix "alpha_") bn_names
-  val alpha_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys
+  val alpha_bn_arg_tys = map (nth raw_tys) bn_tys
   val alpha_bn_tys = map (fn ty => [ty, ty] ---> @{typ "bool"}) alpha_bn_arg_tys
   val alpha_bn_frees = map Free (alpha_bn_names ~~ alpha_bn_tys)
   val alpha_bn_map = bns ~~ alpha_bn_frees
 
-  val constrs_info = all_dtyp_constrs_types descr sorts
-
-  val alpha_intros = map2 (map2 (mk_alpha_intros lthy alpha_map alpha_bn_map)) constrs_info bclausesss 
-  val alpha_bn_intros = map (mk_alpha_bn_intros lthy alpha_map alpha_bn_map constrs_info bclausesss) bn_info
+  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 all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn))
     (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)