--- a/Nominal-General/nominal_library.ML	Tue Aug 17 07:11:45 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Tue Aug 17 17:52:25 2010 +0800
@@ -41,12 +41,12 @@
   val fold_conj: term list -> term
 
   (* datatype operations *)
+  type cns_info = (term * typ * typ list * bool list) list
+
   val all_dtyps: Datatype_Aux.descr -> (string * sort) list -> typ list
   val nth_dtyp: Datatype_Aux.descr -> (string * sort) list -> int -> typ
-  val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> 
-    (term * typ * typ list * bool list) list list
-  val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> 
-    (term * typ * typ list * bool list) list
+  val all_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> cns_info list
+  val nth_dtyp_constrs_types: Datatype_Aux.descr -> (string * sort) list -> int -> cns_info
   val prefix_dt_names: Datatype_Aux.descr -> (string * sort) list -> string -> string list
 
   (* tactics for function package *)
@@ -130,6 +130,8 @@
 
 (** datatypes **)
 
+(* constructor infos *)
+type cns_info = (term * typ * typ list * bool list) list
 
 (* returns the type of the nth datatype *)
 fun all_dtyps descr sorts = 

--- a/Nominal/Ex/SingleLet.thy	Tue Aug 17 07:11:45 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Tue Aug 17 17:52:25 2010 +0800
@@ -25,6 +25,8 @@
 
 thm distinct
 thm trm_raw_assg_raw.inducts
+thm trm_raw.exhaust
+thm assg_raw.exhaust
 thm fv_defs
 thm perm_simps
 thm perm_laws
@@ -37,8 +39,6 @@
 thm size_eqvt
 
 
-(* eqvt lemmas for fv / fv_bn / bn *)
-
 ML {*
   val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct}
 *}
@@ -47,6 +47,14 @@
   val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts}
 *}
 
+ML {* 
+  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw.exhaust}
+*}
+
+ML {* 
+  val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms assg_raw.exhaust}
+*}
+
 ML {*
   val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs}
 *}

--- a/Nominal/NewParser.thy	Tue Aug 17 07:11:45 2010 +0800
+++ b/Nominal/NewParser.thy	Tue Aug 17 17:52:25 2010 +0800
@@ -312,13 +312,15 @@
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo
-  val raw_constrs = 
-    flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts))
+
   val raw_tys = all_dtyps descr sorts
   val raw_full_ty_names = map (fst o dest_Type) raw_tys
   
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names  
  
+  val raw_cns_info = all_dtyp_constrs_types descr sorts
+  val raw_constrs = flat (map (map (fn (c, _, _, _) => c)) raw_cns_info)
+
   val raw_inject_thms = flat (map #inject dtinfos)
   val raw_distinct_thms = flat (map #distinct dtinfos)
   val raw_induct_thm = #induct dtinfo
@@ -349,14 +351,15 @@
 
   val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = 
     if get_STEPS lthy3a > 3 
-    then define_raw_fvs descr sorts raw_bn_info raw_bclauses (raw_inject_thms @ raw_distinct_thms) lthy3a
+    then define_raw_fvs raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses 
+      (raw_inject_thms @ raw_distinct_thms) lthy3a
     else raise TEST lthy3a
 
   (* definition of raw alphas *)
   val _ = warning "Definition of alphas";
   val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
     if get_STEPS lthy3b > 4 
-    then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3b
+    then define_raw_alpha raw_full_ty_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3b
     else raise TEST lthy3b
   val alpha_tys = map (domain_type o fastype_of) alpha_trms  
 

--- 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)

--- a/Nominal/nominal_dt_rawfuns.ML	Tue Aug 17 07:11:45 2010 +0800
+++ b/Nominal/nominal_dt_rawfuns.ML	Tue Aug 17 17:52:25 2010 +0800
@@ -24,9 +24,8 @@
   val setify: Proof.context -> term -> term
   val listify: Proof.context -> term -> term
 
-  val define_raw_fvs: Datatype_Aux.descr -> (string * sort) list -> bn_info ->
-    bclause list list list -> thm list -> Proof.context -> 
-    term list * term list * thm list * thm list * local_theory
+  val define_raw_fvs: string list -> typ list -> cns_info list -> bn_info -> bclause list list list -> 
+    thm list -> Proof.context -> term list * term list * thm list * thm list * local_theory
  
   val raw_prove_eqvt: term list -> thm list -> thm list -> Proof.context -> thm list
 end
@@ -211,26 +210,23 @@
   map2 (mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map) (bn_argss ~~ nth_constrs_info) nth_bclausess
 end
 
-fun define_raw_fvs descr sorts bn_info bclausesss constr_thms lthy =
+fun define_raw_fvs raw_full_ty_names raw_tys cns_info bn_info bclausesss constr_thms lthy =
 let
-  val fv_names = prefix_dt_names descr sorts "fv_"
-  val fv_arg_tys = all_dtyps descr sorts
-  val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;
+  val fv_names = map (prefix "fv_" o Long_Name.base_name) raw_full_ty_names
+  val fv_tys = map (fn ty => ty --> @{typ "atom set"}) raw_tys
   val fv_frees = map Free (fv_names ~~ fv_tys);
-  val fv_map = fv_arg_tys ~~ fv_frees
+  val fv_map = raw_tys ~~ fv_frees
 
   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 fv_bn_names = map (prefix "fv_") bn_names
-  val fv_bn_arg_tys = map (fn i => nth_dtyp descr sorts i) bn_tys
+  val fv_bn_arg_tys = map (nth raw_tys) bn_tys
   val fv_bn_tys = map (fn ty => ty --> @{typ "atom set"}) fv_bn_arg_tys
   val fv_bn_frees = map Free (fv_bn_names ~~ fv_bn_tys)
   val fv_bn_map = bns ~~ fv_bn_frees
 
-  val constrs_info = all_dtyp_constrs_types descr sorts
-
-  val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) constrs_info bclausesss 
-  val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map constrs_info bclausesss) bn_info
+  val fv_eqs = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map)) cns_info bclausesss 
+  val fv_bn_eqs = map (mk_fv_bn_eqs lthy fv_map fv_bn_map cns_info bclausesss) bn_info
   
   val all_fun_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names)
   val all_fun_eqs = map (pair Attrib.empty_binding) (flat fv_eqs @ flat fv_bn_eqs)